def Lean.Meta.iteToDIte (e : Lean.Expr) : Lean.MetaM Lean.Expr

Convert ite expressions in e to dites. It is useful to make this conversion in the WF module because the condition is often used in termination proofs.

Equations

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