where and how are nat and int defined?

Stream: new members

[Robert Watson]

Hi there. I'm following Theorem_Proving_In_Lean_4, but am frustrated because I want to understand what is going on, basics up, even more than application down. I've been looking through data.nat and data.int, but I don't understand where int and nat are actually defined...for example inductively (eg Succ and Zero in some type theories)? Where is it and what am I missing? Perhaps it is some sort of built in functionality? If so how does it work? Where can I get my hands on it properly? That is, where can I best get a real understanding of the most basic (ie most fundamental) aspects of Lean, in addition to the "how to use tactics"-style introductory documentation?

[Chris B]

Nat is in src/init/prelude. If you're using vscode, you should be able to right click on a declaration and click "go to definition".

[Kevin Buzzard]

Have you played the natural number game? This will teach you some basic tactics, and then the definition of the naturals might make some more sense to you.

[Mario Carneiro]

One way to jump to the definition of nat and int is to follow the links -> src#nat src#int

[Robert Watson]

Thanks to all.