Lean keywords

Stream: new members

[Jake Levinson]

Hi all,

Is there a glossary or lexicon of all the Lean keywords and how they work? I've been looking through parts of "Theorem Proving in Lean" (https://leanprover.github.io/theorem_proving_in_lean/) but my issue is that I don't know which parts to look in. For example, is let going to appear under "Propositions and Proofs", "Tactics", "Interacting with Lean", or somewhere else? (I can't just search for let because it appears a lot in the exposition. The word "keyword" doesn't appear I don't think.) Other keywords I'd like to completely understand: instance class show from by namespace... also some tactics, convert refine.

Note: I've done some of the tutorials (natural number game, proof of the intermediate value theorem, some notes from LFCTM2020, some stuff on my own). So I've learned a bunch of the basic "mathy" stuff, like how to split a goal p \and q into two parts and how to use have and obtain, but I don't know much about the "software" aspects (some keywords, wisdom on using placeholders, defining typeclasses, etc) and often don't know how to troubleshoot.

I've also looked in the full API documentation (https://leanprover-community.github.io/mathlib_docs/), but there also, I don't know where to look/search and a lot of it is over my head.

Thanks!
Jake

[Horatiu Cheval]

Does the reference manual work for your purpose of having a glossary?
https://leanprover.github.io/reference/

[Jake Levinson]

That looks helpful! I'll take a look. I somehow didn't realize that was a different document from Theorem Proving in Lean. Maybe that's why I was having trouble finding things, haha.

[Jake Levinson]

Thanks!

[Bryan Gin-ge Chen]

Note that the reference manual hasn't been updated in a long time so some things might be inaccurate.

[Martin Dvořák]

lean-tactics.pdf
This "cheatsheet" could also come handy. However, it is not a comprehensive list of Lean's keywords.

[Alex J. Best]

For mathlib tactics there are pages in the mathlib docs like tactic#convert and tactic#refine

[Kevin Buzzard]

And instance, class, show, from and by are all in #tpil somewhere. show and from very early on, instance and class in the section on typeclasses, and by is just begin...end

[Jake Levinson]

Thanks for the various links!