source
opaque Lean.Meta.Grind.normExt :
SimpExtension
source
def Lean.Meta.Grind.registerNormTheorems (preDeclNames postDeclNames : Array Name) :
MetaM Unit
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

source
def Lean.Meta.Grind.pushNot :
Simp.Simproc
Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For