Zulip Chat Archive

Stream: new members

Topic: where and how are nat and int defined?

Robert Watson (Feb 04 2022 at 22:13):

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 (Feb 04 2022 at 22:18):

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 (Feb 05 2022 at 00:24):

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 (Feb 05 2022 at 01:46):

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

Robert Watson (Feb 05 2022 at 14:24):

Thanks to all.

Last updated: Dec 20 2023 at 11:08 UTC