0
$\begingroup$

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?

enter image description here

Improve this question
$\endgroup$
3

1 Answer 1

Reset to default
2
$\begingroup$

You need to import Std (or more precisely, import Std.Tactic.Ext). In the upcoming stable release of lean, this declaration has moved to Init, so you will no longer have to import Std to get it.

...although, I see now that the example also involves real numbers, which will require import Mathlib.Data.Real.Basic which implies import Std and many other things. Most likely you should just pay attention to the import line from wherever you saw this code snippet.

Improve this answer
$\endgroup$
5
  • $\begingroup$ there are no import lines where I got this. See question edit. $\endgroup$
    – Charlie Parker
    Commented Mar 15 at 19:47
  • $\begingroup$ what does std stand for? $\endgroup$
    – Charlie Parker
    Commented Mar 15 at 19:48
  • $\begingroup$ @CharlieParker Std is the Lean standard library, github.com/leanprover/std4 . It is different from core Lean, and also different from Mathlib. However when you import parts of Mathlib it usually transitively imports large amounts of Std. $\endgroup$
    – Jason Rute
    Commented Mar 15 at 21:31
  • $\begingroup$ In chapter 2 of MIL, when it starts giving code examples, it says: "The import lines at the beginning of the associated examples file import the theory of the real numbers from Mathlib, as well as useful automation. For the sake of brevity, we generally suppress information like this in the textbook." In this case, "the associated examples file" is github.com/leanprover-community/mathematics_in_lean/blob/master/… , which imports the real numbers and other things. $\endgroup$
    – Mario Carneiro
    Commented Mar 17 at 3:18
  • $\begingroup$ But ext is now in Lean 4 core so importing Std is no longer necessary. (You still need Mathlib imports for real numbers.) $\endgroup$
    – François G. Dorais
    Commented Mar 17 at 10:27

Not the answer you're looking for? Browse other questions tagged or ask your own question.