Definition of ℕ (nat)

Stream: general

[Julin S]

Hi.

Where is the nat type defined in lean4?
I couldn't spot it in
https://github.com/leanprover/lean4/blob/master/src/Init/Data/Nat/Basic.lean

Is it compiled in or something?

I am a newbie in lean.

[Christian Merten]

If you search on https://leanprover-community.github.io/mathlib4_docs for Nat, you will get to docs#Nat. If you then click on source on the top right, you get here: https://github.com/leanprover/lean4/blob/744f98064b056ee27fc8c97f524797c8cc96f436/src/Init/Prelude.lean#L1185-L1206.

[Kenny Lau]

@Julin S there are two ways to find out,

1. if you have lean installed, you can do #check Nat, and when you right click the Nat in your code, you'll have an option that says "go to definiton", which will bring you to the file
2. or, you can search Nat on loogle, which will bring you to the docs
   (btw #new members is usually where newbies ask questions)

[Julin S]

Thanks!
Got it: https://github.com/leanprover/lean4/blob/744f98064b056ee27fc8c97f524797c8cc96f436/src/Init/Prelude.lean#L1192

[Julin S]

Sorry had forgotten that newbies channel existed.

[Julin S]

I don't have an lsp set up yet. I guess the 'go to definition' would need that.

[Julin S]

I'm on nvim.

[Kenny Lau]

Julin S said:

I don't have an lsp set up yet. I guess the 'go to definition' would need that.

no, 'go to definition' just searches within your lean, no internet required

[Andrew Yang]

LSP means (part of the) lean vscode (or whatever your editor is) plugin and you will need that for go to definition to work.

[Patrick Massot]

LSP has nothing to do with VSCode and work in nvim

[Patrick Massot]

Julin, you need to install lean.nvim.

[Snir Broshi]

Patrick Massot said:

LSP has nothing to do with VSCode and work in nvim

LSP was invented by the VSCode team, so while nvim does support LSP the claim "LSP has nothing to do with VSCode" is false.

[Patrick Massot]

I almost wrote “except if you do history of software engineering”, but decided it was too much noise.