def Lean.casesOnSuffix : String

Equations

• Lean.casesOnSuffix = "casesOn"

def Lean.recOnSuffix : String

Equations

• Lean.recOnSuffix = "recOn"

def Lean.brecOnSuffix : String

Equations

• Lean.brecOnSuffix = "brecOn"

def Lean.belowSuffix : String

Equations

• Lean.belowSuffix = "below"

def Lean.mkCasesOnName (indDeclName : Name) : Name

Equations

• Lean.mkCasesOnName indDeclName = indDeclName.mkStr Lean.casesOnSuffix

def Lean.mkRecOnName (indDeclName : Name) : Name

Equations

• Lean.mkRecOnName indDeclName = indDeclName.mkStr Lean.recOnSuffix

def Lean.mkBRecOnName (indDeclName : Name) : Name

Equations

• Lean.mkBRecOnName indDeclName = indDeclName.mkStr Lean.brecOnSuffix

def Lean.mkBelowName (indDeclName : Name) : Name

Equations

• Lean.mkBelowName indDeclName = indDeclName.mkStr Lean.belowSuffix

opaque Lean.auxRecExt : TagDeclarationExtension

def Lean.markAuxRecursor (env : Environment) (declName : Name) : Environment

Equations

• Lean.markAuxRecursor env declName = Lean.auxRecExt.tag env declName

def Lean.isAuxRecursor (env : Environment) (declName : Name) : Bool

Equations

• Lean.isAuxRecursor env declName = (Lean.auxRecExt.isTagged env declName || declName == `Eq.ndrec || declName == `Eq.ndrecOn)

def Lean.isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : String) : Bool

Equations

• Lean.isAuxRecursorWithSuffix env (pre.str s) suffix = ((s == suffix || s.startsWith (toString suffix ++ toString "_")) && Lean.isAuxRecursor env (pre.str s))
• Lean.isAuxRecursorWithSuffix env declName suffix = false

def Lean.isCasesOnRecursor (env : Environment) (declName : Name) : Bool

Equations

• Lean.isCasesOnRecursor env declName = Lean.isAuxRecursorWithSuffix env declName Lean.casesOnSuffix

def Lean.isRecOnRecursor (env : Environment) (declName : Name) : Bool

Equations

• Lean.isRecOnRecursor env declName = Lean.isAuxRecursorWithSuffix env declName Lean.recOnSuffix

def Lean.isBRecOnRecursor (env : Environment) (declName : Name) : Bool

Equations

• Lean.isBRecOnRecursor env declName = Lean.isAuxRecursorWithSuffix env declName Lean.brecOnSuffix

def Lean.markSparseCasesOn (env : Environment) (declName : Name) : Environment

Equations

• Lean.markSparseCasesOn env declName = Lean.sparseCasesOnExt✝.tag env declName

def Lean.isSparseCasesOn (env : Environment) (declName : Name) : Bool

Is this a constructor elimination or a sparse casesOn?

Equations

• Lean.isSparseCasesOn env declName = Lean.sparseCasesOnExt✝.isTagged env declName

def Lean.isCasesOnLike (env : Environment) (declName : Name) : Bool

Is this a .casesOn, a constructor elimination or a sparse casesOn?

Equations

• Lean.isCasesOnLike env declName = (Lean.isCasesOnRecursor env declName || Lean.isSparseCasesOn env declName)

inductive Lean.NoConfusionInfo : Type

Shape information for no confusion lemmas. The arity does not include the final major argument (which is not there when the constructors differ) The regular no confusion lemma marks the lhs and rhs arguments for the compiler to look at and find the number of fields. The per-constructor no confusion lemmas know the number of (non-prop) fields statically.

• regular (arity lhs rhs : Nat) : NoConfusionInfo
• perCtor (arity fields : Nat) : NoConfusionInfo

def Lean.instInhabitedNoConfusionInfo.default : NoConfusionInfo

Equations

• Lean.instInhabitedNoConfusionInfo.default = Lean.NoConfusionInfo.regular default default default

instance Lean.instInhabitedNoConfusionInfo : Inhabited NoConfusionInfo

Equations

• Lean.instInhabitedNoConfusionInfo = { default := Lean.instInhabitedNoConfusionInfo.default }

def Lean.NoConfusionInfo.arity : NoConfusionInfo → Nat

Equations

• (Lean.NoConfusionInfo.regular arity lhs rhs).arity = arity
• (Lean.NoConfusionInfo.perCtor arity fields).arity = arity

opaque Lean.noConfusionExt : MapDeclarationExtension NoConfusionInfo

def Lean.markNoConfusion (env : Environment) (n : Name) (info : NoConfusionInfo) : Environment

Equations

• Lean.markNoConfusion env n info = Lean.noConfusionExt.insert env n info

def Lean.isNoConfusion (env : Environment) (n : Name) : Bool

Equations

• Lean.isNoConfusion env n = Lean.noConfusionExt.contains env n

def Lean.getNoConfusionInfo (env : Environment) (n : Name) : NoConfusionInfo

Equations

• Lean.getNoConfusionInfo env n = (Lean.noConfusionExt.find? env n).get!