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

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

Equations

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

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

Similar to simpCore, but uses dsimp.

Equations

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

def Lean.Meta.Grind.preprocess (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.