API reference

Stream: new members

[Arthur Paulino]

Is there an API reference for Lean, containing all its keywords?

[Johan Commelin]

What exactly do you mean by "keyword"? Things like def, theorem, section, set_option, etc??

[Johan Commelin]

Do lists like

    char const * commands[] =
        {"theorem", "axiom", "axioms", "variable", "protected", "private", "hide",
         "definition", "meta", "mutual", "example", "noncomputable", "abbreviation",
         "variables", "parameter", "parameters", "constant", "constants",
         "using_well_founded", "[whnf]",
         "end", "namespace", "section", "prelude",
         "import", "inductive", "coinductive", "structure", "class", "universe", "universes", "local",
         "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
         "set_option", "open", "export", "@[",
         "attribute", "instance", "include", "omit", "init_quotient",
         "declare_trace", "add_key_equivalence",
         "run_cmd", "#check", "#reduce", "#eval", "#print", "#help", "#exit",
         "#compile", "#unify", nullptr};

answer your question?

[Johan Commelin]

That's an excerpt from https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/token_table.cpp

[Arthur Paulino]

That's useful but I also wanted to know what every keyword does

[Eric Wieser]

Note that those are really just the list of builtin "commands", and the list of commands changes at runtime (eg we add command#add_decl_doc which isn't built int)

[Johan Commelin]

Yes, so we need a bit more details about what @Arthur Paulino wants to do with this to be able to help further.

[Johan Commelin]

Is this related to the Prettier project?

[Arthur Paulino]

Johan Commelin said:

Is this related to the Prettier project?

Oh, no no. I am trying to get my head around the native power of lean. I guess I was looking for something similar to this: https://docs.python.org/3/reference/index.html

[Jason Rute]

Try #help commands.

[Jason Rute]

It is important to know that Lean's parser is very flexible and one can add custom user commands to Lean. So if you import all, then #help commands will likely display more commands which were defined in mathlib. Also, it's probably true that there are parts of Lean which are not fully documented (and possibly no one uses anymore, or only a few people use). Nonetheless, starting with Johan's list and #help commands and then searching TPIL, Google, and Zulip for more information will get you started. (Everything I said is for Lean 3 to be clear.)

[Patrick Massot]

Just to make sure: you do know about https://leanprover.github.io/reference/, right?

[Arthur Paulino]

Oh I didn't know about that link!
The Lean landing page takes me to this place when I click on Documentation > Lean 4 manual. But I saw some sections marked with "TODO" or "fix" (like this one) so I thought that it was still a WIP for Lean 4. But I didn't know about that other link which seems to be more finished for Lean 3. Thanks!