Core tactic documentation #
This file adds the majority of the interactive tactics from core Lean (i.e. pre-mathlib) to the API documentation.
Make a PR to core changing core docstrings to the docstrings below, and also changing the docstrings of
convto the ones already in the API docs.
SMT tactics are currently not documented.
constructor_matchingare currently not documented.
dsimpdeserves better documentation.