opaque Lean.Meta.Grind.normExt : SimpExtension

def Lean.Meta.Grind.registerNormTheorems (preDeclNames postDeclNames : Array Name) : MetaM Unit

Equations

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

def Lean.Meta.Grind.simpEq : Simp.Simproc

Equations

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

def Lean.Meta.Grind.simpDIte : Simp.Simproc

Equations

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

def Lean.Meta.Grind.pushNot : Simp.Simproc

def Lean.Meta.Grind.simpOr : Simp.Simproc

Equations

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

def Lean.Meta.Grind.reduceCtorEqCheap : Simp.Simproc

Equations

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

def Lean.Meta.Grind.unfoldReducibleSimproc : Simp.DSimproc

Equations

• Lean.Meta.Grind.unfoldReducibleSimproc e = liftM (Lean.Meta.Grind.unfoldReducibleStep e)

def Lean.Meta.Grind.getSimprocs : MetaM (Array Simprocs)

Returns the array of simprocs used by grind.

Equations

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

def Lean.Meta.Grind.getSimpContext (config : Grind.Config) : MetaM Simp.Context

Returns the simplification context used by grind.

Equations

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

@[export lean_grind_normalize]

def Lean.Meta.Grind.normalizeImp (e : Expr) (config : Grind.Config) : MetaM Expr

Equations

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