source
def reduceIte :
Lean.Meta.Simp.Simproc
Equations

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

Instances For

source
def reduceDIte :
Lean.Meta.Simp.Simproc
Equations

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

Instances For

source
def dreduceIte :
Lean.Meta.Simp.DSimproc
Equations

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

Instances For

source
def dreduceDIte :
Lean.Meta.Simp.DSimproc
Equations

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

Instances For

source
def reduceCtorEq :
Lean.Meta.Simp.Simproc
Equations

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

Instances For