central list of tactics and what they're good for?

Stream: general

[Alex Kontorovich]

With new tactics coming online all the time (which is great!), it's getting harder and harder to keep track. Is there a central list of tactics, perhaps organized by what kinds of problems they work on, and some well-chosen examples of their use in practice?

[Yaël Dillies]

It's coming soon!

[Yaël Dillies]

Oh, looks like it's online already, but I doubt it's been announced, so use at your own risks: https://leanprover-community.github.io/mathlib-manual/html-multi/

[Alex Kontorovich]

Wow, that was fast! :)

[Asei Inoue]

I’m writing a reference too (Japanese only)

https://lean-ja.github.io/lean-by-example/Tactic/index.html

which has a lot of example codes

[Alok Singh]

Asei Inoue said:

I’m writing a reference too (Japanese only)

https://lean-ja.github.io/lean-by-example/Tactic/index.html

which has a lot of example codes

maybe AI translation could help here?

[Asei Inoue]

@Alok Singh maybe. copy-paste to ChatGPT and ask translation.