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

• Lean.Meta.Grind.pushNewFact proof generation = do let prop ← liftM (Lean.Meta.inferType proof) Lean.Meta.Grind.pushNewFact' prop proof generation