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 a Nat.hasNotBit mask x.ctorIdx hypothesis to express that these constructors were not matched. Using a single hypothesis like this, rather than many hypotheses of the form x.ctorIdx ≠ i, is important to avoid quadratic overhead in code like match splitter generation.

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 a more sophisticated implementation 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.