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.

Instances For