This modules defines the CasesInfo data structure and functions to obtain it. It contains information about the structure of casesOn-like functions, namely of

• Plain .casesOn (one alternative per constructor)
• Per-constructor eliminiations (with side condition, one alternative only)
• Sparse cases-on (only some constructors, with a catch-all)

It recognizes .casesOn by using isCasesOnRecursor (name + isAuxDecl env ext), and the others via the isSparseCasesOn env ext.

It is used in particular by the code generator to replace calls to such functions with LCNF's cases construct.

The getSparseCasesInfo? function calculates the CasesInfo from the type of the declaration, and makes certian assumptions about their shapes. If this is too fragile, the sparseCasesOn env extension could carry more information from which the shape can be calculated..

inductive CasesAltInfo : Type

• ctor (ctorName : Lean.Name) (numFields : Nat) : CasesAltInfo
• default (numHyps : Nat) : CasesAltInfo

def instInhabitedCasesAltInfo.default : CasesAltInfo

Equations

• instInhabitedCasesAltInfo.default = CasesAltInfo.ctor default default

instance instInhabitedCasesAltInfo : Inhabited CasesAltInfo

Equations

• instInhabitedCasesAltInfo = { default := instInhabitedCasesAltInfo.default }

structure CasesInfo : Type

Information about the shape of casesOn-like declarations.

We treat them uniformly in the code generator.

• declName : Lean.Name
• indName : Lean.Name
• arity : Nat
• discrPos : Nat
• altsRange : Std.Rco Nat
• altNumParams : Array CasesAltInfo

def CasesInfo.numAlts (c : CasesInfo) : Nat

Equations

• c.numAlts = c.altNumParams.size

def getCasesInfo? (declName : Lean.Name) : Lean.CoreM (Option CasesInfo)

Equations

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