@[extern lean_mk_cases_on]

opaque Lean.mkCasesOnImp (env : Kernel.Environment) (declName : Name) : Except Kernel.Exception Declaration

def Lean.isCasesOnViaProjs (declName : Name) : MetaM Bool

Whether casesOn for declName is built by mkCasesOnViaProjs? rather than from the recursor.

A single constructor and no indices make the type structure-like, and large elimination then forces every field to be a proof, which is what makes the projections available: projecting data out of a proposition is what Exists may not do.

Equations

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

def Lean.mkCasesOnViaProjs? (declName : Name) : MetaM (Option DefinitionVal)

Builds a casesOn-shaped eliminator for declName out of structure projections, or returns none if isCasesOnViaProjs does not hold.

I.casesOn … t minor as built from I.rec reduces only once t reduces to a constructor application, which for a proposition it may never do: proofs are opaque. Applying the minor premise to the projections of t instead sidesteps that. The minor premise expects the fields of I.mk x₁ … xₙ rather than those of t, but both are proofs of the same proposition, so proof irrelevance identifies them.

The result has the same shape as mkCasesOnImp produces: parameters, motive, major premise, minor premise. It also matches recOn, since the type is not recursive.

Equations

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

def Lean.mkCasesOn (declName : Name) : MetaM Unit

Equations

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