Started up VSCode today and errors...

Stream: lean4

[Daniel Donnelly]

image.png

Anyway around these? I really like entering in \N for Nat etc because of the math realism in it. For that in VSCode I have another extension installed.

[Martin Dvořák]

For ℕ to be valid, you have to import something. This notation is not in the core. Try #check Nat instead.

[Martin Dvořák]

import Mathlib.Init.Data.Nat.Basic

[Eric Wieser]

The notation is provided by Mathlib.Init.Data.Nat.Notation

[Eric Wieser]

In Lean 3, it was provided by Lean itself