Fancy N problem

Stream: new members

[E. M. Eisner]

I have just downloaded Lean4 and am trying to go through the Mathematics in Lean tutorial. However, when I started trying to do the tutorial I ran into a problem which was that the documentation uses the fancy \mathbb N but then the editor vscode said that it wasn't in scope. It seemed that when I changed it to Nat it worked. Does anyone know what's going on here?

[Matt Diamond]

Have you tried adding an import to the top, like import Mathlib?

[E. M. Eisner]

nope! will try! (don't think that the tutorial told me to do that)

[Patrick Massot]

There shouldn’t be any need to add any import. What is the file that has this issue?

[Eric Wieser]

I get the feeling that @E. M. Eisner has created a new blank file

[Patrick Massot]

Ah, this would indeed explain everything. This is no what is recommended to read the book. You may need to read again the setup explanations at the very beginning.

[E. M. Eisner]

No that is not what happened. I was in the very first file with #eval "Hello, World!" in it... I just added the first couple examples from section 1.2 of the book and got an error from the fancy \mathbb N

[Matt Diamond]

Ah, that's the issue then. You're meant to open the file S02_Overview.lean instead of adding the examples from that section to S01_Getting_Started.lean. The "Getting Started" file has no imports, which is why it didn't work. S02_Overview.lean has the appropriate imports at the top.

[Patrick Massot]

Each section of the book has its Lean file. Nothing will work if you edit the wrong file.

[E. M. Eisner]

okay well i missed that instruction i guess - thanks for letting me know!