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

$\endgroup$
3

1 Answer 1

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.

$\endgroup$
5
  • $\begingroup$ there are no import lines where I got this. See question edit. $\endgroup$ Mar 15 at 19:47
  • $\begingroup$ what does std stand for? $\endgroup$ 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
    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$ 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$ Mar 17 at 10:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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