Documentation
Lean
.
Meta
.
Tactic
.
Simp
.
BuiltinSimprocs
.
Core
Search
Google site search
return to top
source
Imports
Init.Simproc
Lean.Meta.Tactic.Simp.Simproc
Imported by
reduceIte
reduceDite
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