feat: add `grind` tactic This PR adds the (WIP) `grind` tactic. It currently generates a warning message to make it clear that the tactic is not ready for production.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean (documentation source: doc/make/index.md).