def Lean.Meta.Grind.isLegacyNormalizer : CoreM Bool

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

Equations

• Lean.Meta.Grind.isLegacyNormalizer = do let __do_lift ← Lean.getOptions pure (Lean.Option.get __do_lift Lean.Meta.Grind.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.

Equations

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

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

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

Equations

• Lean.Meta.Grind.simpCore e = do let __do_lift ← liftM Lean.Meta.Grind.isLegacyNormalizer if __do_lift = true then Lean.Meta.Grind.legacySimpCore✝ e else Lean.Meta.Grind.symSimpCore✝ e

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

Similar to simpCore, but uses dsimp.

Equations

• Lean.Meta.Grind.dsimpCore e = do let __do_lift ← liftM Lean.Meta.Grind.isLegacyNormalizer if __do_lift = true then Lean.Meta.Grind.legacyDSimpCore✝ e else Lean.Meta.Grind.symDSimpCore✝ e

@[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.

Equations

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

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

Equations

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

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.

Equations

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

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.

Equations

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