Mathlib4 Tactics

This is a list of the output of #help command of mathlib4. see GitHub Page!

This is heavily inspired by haruhisa-enomoto/mathlib4-all-tactics.

This web page is automatically updated by GitHub Action.

How to generate markdown file

First, install Lean and Python 3.10, and then run the following commands:

rm .\src\tactics.md
lake env lean --run Tactic.lean > src/tactics.md
python3 script.py