A short introduction to the grind tactic

9. Sources and Resources🔗

As mentioned many times, you should read the relevant section in the Language Reference to get a general overview of how grind works with a lot more detail than presented here.

For grind interactive mode see this talk by Kim Morrison (especially to see examples) and the Lean 4.25.0 release notes.

For custom grind sets and local grind see the Lean 4.28.0 release notes.

For style suggestions for grind see these suggestions by Chris Henson.