List of commands

Stream: general

[Paul Lezeau]

Is there anywhere a list of commands a bit similar to the list of tactics in the Mathlib manual?
E.g. something that lists commands that are generally useful when writing proofs, e.g. #check, #synth, etc
(if not, I'd be happy to start one!)

[Aaron Liu]

I know of this, which is an automatically generated list of all the commands in mathlib + dependencies.

[Paul Lezeau]

Nice! I think it could be nice to have something with a little more documentation and examples in the manual (edit: for beginners)

[Damiano Testa]

Maybe you already know this, but

import Mathlib

#help command

generates a list of all the commands with all their doc-strings.

[Damiano Testa]

You can then filter by matching prefix: #help command "ali" will show all forms of alias.

[Paul Lezeau]

Good point! I guess what I have in mind is something a bit more targeted towards beginners that might not know where to look exactly (and which commands are the most relevant to what they're doing)

[Damiano Testa]

I fully agree that a curated list of [whatever] is a great idea! I view #help as a good starting point, since it is always up to date and will already contain what should be at least the bare minimum documentation.