Lean 4 basic error

Stream: lean4

[Alexandre Rademaker]

Documentation of Lean 4 is quite incomplete yet. I may be doing something silly. But

import Init.Data.Nat
open Nat

def test0 (n : ℕ) := n

def test1 (n : Nat) := n

gives the error "unknown identifier 'ℕ'" (both in VS and Emacs). The second definition works fine. Any idea? Any pointers to learn more about Lean 4?

[Arthur Paulino]

Try adding abbrev ℕ := Nat before using ℕ

Also, you shouldn't need the

import Init.Data.Nat
open Nat

part for it to work

[Leonardo de Moura]

ℕ is defined in Mathlib 4.
For documentation, the best source is https://leanprover.github.io/theorem_proving_in_lean4/

[Alexandre Rademaker]

thanks

[Adam Topaz]

FYI, the way that mathlib4 defines this notation is as follows:
notation "ℕ" => Nat

[Arthur Paulino]

Adam Topaz said:

FYI, the way that mathlib4 defines this notation is as follows:
notation "ℕ" => Nat

Nice one. What are the differences between those methods? (comparing with abbrev)

[Alexandre Rademaker]

Indeed, notation "ℕ" => Nat makes both definitions have the sameℕ → ℕ type. With abbreviation makes one Nat → Nat and the other ℕ → ℕ

[Adam Topaz]

I don't know the inner workings, but if it's similar to Lean3, then abbreviation essentially means @[reducible, inline] def

[Alexandre Rademaker]

But @Arthur Paulino this is not an explanation, just my description of the observable behaviour. The documentation pointed by @Leonardo de Moura should explain us more...

[Horatiu Cheval]

Alexandre Rademaker said:

Indeed, notation "ℕ" => Nat makes both definitions have the sameℕ → ℕ type. With abbreviation makes one Nat → Nat and the other ℕ → ℕ

I guess that's because with abbrev, \N is a new term, even though definitionally equal with Nat, and very transparently so, but still a different term. While with notation it's just syntax that gets desugared to the exact same thing.