def Lean.Meta.Grind.isLegacyNormalizer : CoreM Bool

Returns true if the legacy simp-based normalizer is selected (backward.grind.normalizer).

def Lean.Meta.Grind.symNorm (e : Expr) (methods : Sym.Simp.Methods) (dmethods : Sym.DSimp.Methods) (s : Sym.Simp.State) (ds : Sym.DSimp.State) : Sym.SymM (Simp.Result × Sym.Simp.State × Sym.DSimp.State)

The Sym.simp-based normalization step: Sym.simp with methods, then Sym.dsimp of the result with dmethods. The two passes are independent, and their states are threaded through.

Sym.simp does not visit the fixed arguments of an application, e.g. the implicit objects of a morphism composition, while the legacy normalizer dsimps them (Simp.Config.dsimp). A beta-redex or a projection of a structure instance left in such an argument makes the term miss the E-matching patterns of its theorems, so the dsimp pass reduces them. Its result is definitionally equal to the simp result, so the proof is the one of the simp pass.

Sym requires kernel projections to be folded into projection applications. The legacy normalizer accepts them, so preprocessImpl folds them only afterwards; they are folded here first.

def Lean.Meta.Grind.simpCore (e : Expr) : GrindM Simp.Result

Simplifies the given expression using the grind simprocs and normalization theorems.

def Lean.Meta.Grind.dsimpCore (e : Expr) : GrindM Expr

Similar to simpCore, but uses dsimp.

@[export lean_grind_preprocess]

def Lean.Meta.Grind.preprocessImpl (e : Expr) : GoalM Simp.Result

Preprocesses e using grind normalization theorems and simprocs, and then applies several other preprocessing steps.

def Lean.Meta.Grind.pushNewFact' (prop proof : Expr) (generation : Nat := 0) : GoalM Unit

def Lean.Meta.Grind.pushNewFact (proof : Expr) (generation : Nat := 0) : GoalM Unit

Infers the type of the proof, preprocess it, and adds it to todo list.

def Lean.Meta.Grind.preprocessLight (e : Expr) : GoalM Expr

A lighter version of preprocess which produces a definitionally equal term, but ensures assumptions made by grind are satisfied.