Zulip Chat Archive

Stream: new members

Topic: Lean keywords


Jake Levinson (Aug 09 2021 at 16:07):

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 (Aug 09 2021 at 16:30):

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

Jake Levinson (Aug 09 2021 at 16:34):

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 (Aug 09 2021 at 16:34):

Thanks!

Bryan Gin-ge Chen (Aug 09 2021 at 16:37):

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

Martin Dvořák (Aug 09 2021 at 16:49):

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

Alex J. Best (Aug 09 2021 at 18:02):

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

Kevin Buzzard (Aug 09 2021 at 19:28):

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 (Aug 10 2021 at 03:34):

Thanks for the various links!


Last updated: Dec 20 2023 at 11:08 UTC