3
$\begingroup$

I'm wondering if Lean 4 tactics are documented anywhere, in a way comparable to the API documentation for mathlib.

(Sorry for brevity...will edit if this is unclear.)

$\endgroup$
6
  • $\begingroup$ On the web or from within Lean? On the web there was a list for Lean 3, and I don’t know why it is taking so long to make one for Lean 4. From within Lean, you can do #print tactic (you need import Mathlib). $\endgroup$
    – Jason Rute
    Commented May 17 at 18:52
  • $\begingroup$ Also it is a bit annoying to cross post questions without letting others know you are doing it: leanprover.zulipchat.com/#narrow/stream/113489-new-members/… It leads to duplicate work. $\endgroup$
    – Jason Rute
    Commented May 17 at 18:52
  • $\begingroup$ @Jason Rute, you are right. It occurred to me after posting this that the question was better for Zulip. Should I delete this question? $\endgroup$
    – Jon Bannon
    Commented May 17 at 19:00
  • 2
    $\begingroup$ This question is fine here. Once there's an answer, this is a more permanent place for it. $\endgroup$ Commented May 17 at 19:11
  • $\begingroup$ Maybe raw.githubusercontent.com/haruhisa-enomoto/mathlib4-all-tactics/… ? $\endgroup$ Commented May 17 at 19:39

1 Answer 1

5
$\begingroup$

You can use #help tactic (after import Mathlib.Tactic.HelpCmd) to list all tactics available in the current environment. You may also want to import Mathlib.Tactic.Common to make sure mathlib's basic tactics are available, and import Mathlib.Tactic for the kitchen sink.

There is also https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md, which is the result of postprocessing the output of #help tactic into markdown form.

This list is automatically generated and just contains the hover documentation for each tactic, so it's not particularly high quality (it includes some semi-internal tactics and tactic combinators, and sometimes the same tactic appears multiple times because it is internally represented as multiple tactics with the same start token and different following syntax, or slight variations on the same tactic). Lean 3 had a specifically curated tactics page but this has not been replicated in lean 4 yet.

$\endgroup$
1
  • $\begingroup$ Thanks, Mario! I will accept this answer because it indeed answers the title question, as things currently are. $\endgroup$
    – Jon Bannon
    Commented May 18 at 14:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.