def Lean.Meta.Grind.simpCore (e : Lean.Expr) : Lean.Meta.Grind.GrindM Lean.Meta.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.simp (e : Lean.Expr) : Lean.Meta.Grind.GrindM Lean.Meta.Simp.Result

Simplifies 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.