Nat vs ℕ

Stream: new members

[Tyler Josephson ⚛️]

If I don't have any imports, I need to use Nat in this function; I can't use ℕ.
Nonetheless, I can still use ℕ to define a variable.

If I import Mathlib, then I can use ℕ in the function. What's going on?

variable (x :ℕ )

def factorial : ℕ  → ℕ
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

[Yury G. Kudryashov]

Notation ℕ is defined in Mathlib. Without any imports, this is just a random symbol. You can declare a variable of this type, because you have set_option autoImplicit true (default value, switched off in Mathlib), so Lean will add an implicit {ℕ : Sort _}.

[Kyle Miller]

You can hover over ℕ in variable (x : ℕ) to see that it's not Nat