Definition of Nat in Lean4 library

Stream: Lean for teaching

[Mukesh Tiwari]

Hi everyone, trivial question: I am looking for definition of Natural numbers. I looked into the src/Init/Data/Nat but I could not find anything. Could you please point me towards the definition of Nat.

[Henrik Böving]

Its in Prelude.lean: docs4#Nat

[Henrik Böving]

You could've also figured this out by using your editors go to definition feature on Nat, it will follow built-ins^^

In general this is only the Nat definition the Lean user will see, internally it is done with GMP integers