Zulip Chat Archive

Stream: Lean for teaching

Topic: Definition of Nat in Lean4 library

Mukesh Tiwari (Jul 06 2022 at 06:46):

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 (Jul 06 2022 at 06:53):

Its in Prelude.lean: docs4#Nat

Henrik Böving (Jul 06 2022 at 06:55):

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

Last updated: Dec 20 2023 at 11:08 UTC