List of important keywords

Stream: new members

[Adomas Baliuka]

I recently learned about the "list of all tactics" (github). It's sorted alphabetically, not by "commonness" or "typo of situation to use in", but it's still great to have. I think the learning materials (e.g. manual, books) should mention it.

Is there something analogous that lists all keywords of the base language? I'm wondering, for example, where I can find out about the difference between defand abbrev. (Note: I do want to know the difference, but my question is really where to find answers to such questions)

[Eric Wieser]

Ideally you would just type each into the editor, and inspect the documentation that appears when you hover over them

[Adomas Baliuka]

@Eric Wieser most of them give no documentation at all. Such as abbrev or def or noncomputable.... Some do work, for example lemma tells you it's the same as theorem

[Kevin Buzzard]

At least this is a more reasonable task than trying to grok all tactics (of which there are dozens); my feeling is that there are only a few keywords. I think I've just picked them all up by osmosis and #tpil .

[Eric Wieser]

Optimistically then this could be fixed by a PR that just adds docstrings to lean4 itself where those commands are defined?

[Kevin Buzzard]

Would such PRs be accepted? Personally I don't like how declarations like docs#Nat.gcd don't have a docstring and would happily PR them.

[Kevin Buzzard]

I take marks off students for writing definitions with no docstrings, so it's a shame to see it happening for definitions which they're using.

[Adomas Baliuka]

As a new user, I would love more docstrings.

Some things might also deserve something like a manual page. For example "all keywords (ways?) to declare functions/Propositions/classes and the differences between them". It feels to me like most (but not all) of these keywords are just redundant conveniences (e.g. probably theoremand certainly lemma). For example, I wonder if it's possible to define a type class without the classkeyword, since the "Functional Programming" book says that classes are really "just" inductive types. But I don't know where to look for such details.

[Kevin Buzzard]

#tpil defines almost all keywords and gives lengthy explanations and examples (for example it explains how classes are really just inductive types)

[Notification Bot]

67 messages were moved from this topic to #mathlib4 > lemma vs theorem by Eric Wieser.

[Utensil Song]

The following message is manually moved back from #mathlib4 > lemma vs theorem because personally, I want to dig deeper into this issue of understanding the keywords and symbols, but the following is the best I can do for now.

While #tpil is the most valuable book to read and understand what's under the hood of Lean and how they form high level abstractions, if you're looking for a list of "keywords" (which is hard to search) or "symbols" (even harder to search), they are mostly in the source of Lean 4 here: Lean.Parser, most of them are in Term.lean and Command.lean. They are declared here then implemented in Lean.Elab but it has less doc and is less readable there. The good thing is that you can search them better in these files with something like «fun» or "fun", and you can find them in Mathlib4 doc too like Lean.Parser.Command.def or Parser.Term.fun, but the source is better. You'll have a direct idea about how different are they parsed and elaborated, or it might be just one calling the other.

I also find GPT-4 has good knowledge about Lean 4 syntax and notations, I usually paste a random code from Mathlib4 and ask it to explain the code for each keyword, notation or tactics depending on what I don't understand. Or just ask the differences between two keywords etc. and it gives good result as long as you quote them with `, and you can even ask for examples. Sometimes the answer could be misleading, so remember to cross-check what it's telling you with Zulip search or doc/book search. In some cases, all it can give you is the inspiration of how to search.