Documentation

Lean.Elab.Tactic.Grind.Norm

The grind_norm tactic is a debugging aid for the migration of the grind normalizer to Sym.simp. It will be deleted once the migration is complete.