I get this error:
unknown attribute [ext]
and my code is literally a copy paste of the code from mathematics in lean:
-- define a point using structures in lean4
@[ext]
structure Point where
x : ℝ
y : ℝ
z : ℝ
#check Point
what is going on? How do I fix this?