Lean 4 tactics list

Stream: new members

[Jon Bannon]

Is there an encyclopedic list of Lean 4 tactics? I expect I am not looking in the right places...

[Kevin Buzzard]

A slightly out-of-date one is https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md

[Jon Bannon]

Thank you, Kevin. Sorry for the multi-post!

[Kevin Buzzard]

I'm pretty sure someone else did a more recent version. I think that perhaps the only reason this isn't on some official site is that people haven't figured out how to auto-update it.

[Luigi Massacci]

If I’m not mistaken, the stuff in Mathlib.Tactic should in fact be all the tactics (note that the file itself won’t appear to contain anything in the docs, but everything is in the subdirectory on the left)

[Kyle Miller]

@Luigi Massacci There are more tactics in Lean and in Std beyond those.

We really need the documentation to show an encyclopedic list of all the tactics. The information is inside all the compiled files somewhere, but the work needs to be done.

[Jason Rute]

When there is a canonical answer, put it here: https://proofassistants.stackexchange.com/q/3986/122

[Luigi Massacci]

Kyle Miller said:

Luigi Massacci There are more tactics in Lean and in Std beyond those.

and I used omega this morning too🤦🏻‍♂️

[Jon Bannon]

@Jason Rute : I can also delete that stackexchange post if it is better to collect things here. Just let me know.

[Luigi Massacci]

I think having a non Zulip answer is probably a good idea