instances of nat

Stream: lean4

[Jiatong Yang]

def isSame (l : List ℕ) : Bool := l.all (λx => x == l.head!)
Why Lean4 cannot synthesize instance Inhabited ℕ or BEq ℕ?

[Mario Carneiro]

because the ℕ syntax is not declared (it probably looks blue / variable colored in vscode)

[Mario Carneiro]

it's spelled Nat if you don't have mathlib4 imported

[Jiatong Yang]

Oh, thank you!

[Jiatong Yang]

I prefer lean4's syntax, but it seems that it is still a long time before mathlib4 can be put into use. :sob:

[Jiatong Yang]

Is there a way to use lean3's mathlib in lean4?

[Scott Morrison]

Jiatong Yang said:

Is there a way to use lean3's mathlib in lean4?

We're working on it... :-) But it's a huge task, with many moving parts. Have a look at the stream mathlib4 for progress.