Documentation

Lean.Elab.PreDefinition.WF.Ite

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