def Lean.Meta.Sym.Simp.simpCond : Simproc

Simplifies a cond expression (aka Boolean if-then-else).

Equations

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

def Lean.Meta.Sym.Simp.simpControl : Simproc

Simplifies control-flow expressions such as if-then-else and match expressions. It visits only the conditions and discriminants.

Equations

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

def Lean.Meta.Sym.Simp.reduceControl : Simproc

Like simpControl, but does not block the simplifier: when the condition or the discriminants are not decided, the branches are visited too.

Equations

• Lean.Meta.Sym.Simp.reduceControl e = do let __do_lift ← Lean.Meta.Sym.Simp.simpControl e pure __do_lift.markAsNotDone