Open cireu opened 1 month ago
structure Point (α : Type u) where
mk :: (x : α) (y : α)
deriving Repr
/- test -/
#check Point -- a Type
#check @Point.rec -- the eliminator
#check @Point.mk -- the constructor
#check @Point.x -- a projection
#check @Point.y -- a projection
#eval Point.x (Point.mk 10 20)
#eval Point.y (Point.mk 10 20)
It seems that Github can render this correct.
I test the Lean 4 in Shiki at https://shiki.matsu.io/
And I found Shiki cannot render the
--
comment of Lean correctly.(See the different between
/- test -/
and-- comment
).