Britt Anderson and Unicode Issue

Stream: new members

[Britt Anderson]

Greetings. I am a cognitive neuroscientist interested in the idea of writing cognitive models in a language where one can, in principle, verify claims, but that one can also just use for scientific computing. So, I decided to try it out.

One minor snafu I am having is that the unicode/blackboard characters appear in my IDE (both emacs and vscode), but in neither are they recognized.
For example, the first line below is fine. The second I produced by typing "\N" (without quotes), but it is being treated as a different type. If I hover over the "Nat" it tells me "Type" if I hover over the blackboard N I get "Type u_1". I can just type out the full names, but it would be nice to get this working. Anyone have an idea what setting I fouled up? Thanks.

def a : Nat := 3

def b : ℕ := 4

[Edward van de Meent]

the issue is likely that that the notation which makes lean recognise ℕ as Nat is defined as part of mathlib. importing the relevant part of mathlib should solve this issue.

[Julian Berman]

You don't need to import anything, but you do need to be in a project which depends on Mathlib, I believe. E.g. you need to have run lake init math to use the Mathlib template, or to otherwise have it in your lakefile.lean. It seems I'm incorrect then.

[Edward van de Meent]

if you open the snippet in the playground, it throws an error, while starting off the file with import Mathlib solves it... i think that means that it is defined somewhere in mathlib (or one of mathlibs dependencies?)

[Ruben Van de Velde]

You do need to import the relevant Mathlib file

[Ruben Van de Velde]

Mathlib.Data.Nat.Notation

[Julian Berman]

Interesting, I thought it was in Mathlib's Init.

[Britt Anderson]

That solves it.
I did create a project to make sure I had Mathlib then,

import Mathlib.Data.Nat.Notation

def hello := "world"

def a : ℕ := 3

def myadd (x y : ℕ) : ℕ := x + y

#eval myadd 2 3

And all works as expected. Thank you everyone.

[Ruben Van de Velde]

There's no files in mathlib that would be imported implicitly as far as I'm aware