Documentation

Lean.Elab.PreDefinition.WF.Ite

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.