See mkSparseCasesOn below.

def Lean.Meta.mkSparseCasesOn (indName : Name) (ctors : Array Name) : MetaM Name

This module creates sparse variants of casesOn that have arms only for some of the constructors, offering a catch-all.

The minor arguments come in the order of the given ctors array.

The catch-all provides x.ctorIdx ≠ i hypotheses for each constructor i that is matched.

This function is implemented with a simple call to .rec, i.e. no clever branching on the constructor index. The compiler has native support for these sparse matches anyways, and kernel reduction would not benefit from from a more sophisticated implementan unless it has itself native support for .ctorIdx and constructor elimination functions.

Equations

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