See mkSparseCasesOn below.

structure Lean.Meta.SparseCasesOnInfo : Type

Information necessary to recognize and split on sparse casesOn (in particular in MatchEqs)

• indName : Name
• majorPos : Nat
• arity : Nat
• insterestingCtors : Array Name

instance Lean.Meta.instInhabitedSparseCasesOnInfo : Inhabited SparseCasesOnInfo

Equations

• Lean.Meta.instInhabitedSparseCasesOnInfo = { default := Lean.Meta.instInhabitedSparseCasesOnInfo.default }

def Lean.Meta.instInhabitedSparseCasesOnInfo.default : SparseCasesOnInfo

Equations

• Lean.Meta.instInhabitedSparseCasesOnInfo.default = { indName := default, majorPos := default, arity := default, insterestingCtors := default }

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.

def Lean.Meta.getSparseCasesOnInfoCore (env : Environment) (sparseCasesOnName : Name) : Option SparseCasesOnInfo

Equations

• Lean.Meta.getSparseCasesOnInfoCore env sparseCasesOnName = Lean.Meta.sparseCasesOnInfoExt✝.find? env sparseCasesOnName

def Lean.Meta.getSparseCasesOnInfo (sparseCasesOnName : Name) : CoreM (Option SparseCasesOnInfo)

Equations

• Lean.Meta.getSparseCasesOnInfo sparseCasesOnName = do let env ← Lean.getEnv pure (Lean.Meta.sparseCasesOnInfoExt✝.find? env sparseCasesOnName)