Baffling error: unknown identifier

Stream: new members

[Kevin Cheung]

Why does Lean complain that ℕ is an unknown identifier in the second line but not the first line?
Screenshot-2024-01-23-at-7.59.54AM.png

[Damiano Testa]

I think that the notation for Nat is defined in Mathlib: try importing (almost) anything from Mathlib and it should work.

[Kevin Cheung]

Thank you. It worked.

[Kevin Cheung]

The reason it doesn't complain about the first line is because it treats ℕ as an arbitrary type? (i.e. it could have been some other letter, say Q?)

[Ruben Van de Velde]

Yeah, I think so. Try #check f

[Damiano Testa]

That has to do with autoImplicits. If you add set_option autoImplicit false at the beginning of the file, it will error earlier.

[Kevin Cheung]

Thanks to both of you. This is very helpful.