Entry point of the grind normalizer at attribute time, selecting the legacy simp-based normalizer or the Sym.simp-based one by backward.grind.normalizer. The GrindM entry points (simpCore, dsimpCore) dispatch in Lean.Meta.Tactic.Grind.Simp.

@[export lean_grind_normalize]

def Lean.Meta.Grind.normalizeImp (e : Expr) (config : Grind.Config) : MetaM Expr

Normalizes e at attribute time (E-matching patterns).

Equations

• One or more equations did not get rendered due to their size.