def Lean.casesOnSuffix : String

def Lean.recOnSuffix : String

def Lean.brecOnSuffix : String

def Lean.belowSuffix : String

def Lean.mkCasesOnName (indDeclName : Name) : Name

def Lean.mkRecOnName (indDeclName : Name) : Name

def Lean.mkBRecOnName (indDeclName : Name) : Name

def Lean.mkBelowName (indDeclName : Name) : Name

opaque Lean.auxRecExt : TagDeclarationExtension

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

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

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

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

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

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

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

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

Is this a constructor elimination or a sparse casesOn?

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

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

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

instance Lean.instInhabitedNoConfusionInfo : Inhabited NoConfusionInfo

def Lean.NoConfusionInfo.arity : NoConfusionInfo → Nat

opaque Lean.noConfusionExt : MapDeclarationExtension NoConfusionInfo

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

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

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