See mkCasesOnSameCtor below.

def Lean.mkCasesOnSameCtorHet (declName indName : Name) : MetaM Unit

Helper for mkCasesOnSameCtor that constructs a heterogenous matcher (indices may differ) and does not include the equality proof in the motive (so it's not a the shape of a matcher) yet.

Equations

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

def Lean.mkCasesOnSameCtor (declName indName : Name) : MetaM Unit

This constructs a matcher for a match statement that matches on the constructors of a data type in parallel. So if h : x1.ctorIdx = x2.ctorIdx, then it implements

match x1, x2, h with
| ctor1 .. , ctor1 .. , _ => ...
| ctor2 .. , ctor2 .. , _ => ...

The normal matcher supports such matches, but implements them using nested casesOn, which leads to a quadratic blow-up. This function uses the per-constructor eliminators to implement this more efficiently.

This is useful for implementing or deriving functionality like BEq, DecidableEq, Ord and proving their lawfulness.

One could imagine a future where match compilation is smart enough to do that automatically; then this module can be dropped.

Note that for some data types where the indices determine the constructor (e.g. Vec), this leads to less efficient code than the normal matcher, as this needs to read the constructor tag on both arguments, wheras the normal matcher produces code that reads just the first argument’s tag, and then boldly reads the second argument’s fields.

Equations

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