def Lean.casesOnSuffix : String

def Lean.recOnSuffix : String

def Lean.brecOnSuffix : String

def Lean.binductionOnSuffix : String

def Lean.belowSuffix : String

def Lean.ibelowSuffix : String

def Lean.mkCasesOnName (indDeclName : Name) : Name

def Lean.mkRecOnName (indDeclName : Name) : Name

def Lean.mkBRecOnName (indDeclName : Name) : Name

def Lean.mkBInductionOnName (indDeclName : Name) : Name

def Lean.mkBelowName (indDeclName : Name) : Name

def Lean.mkIBelowName (indDeclName : Name) : Name

opaque Lean.auxRecExt : TagDeclarationExtension

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

@[export lean_is_aux_recursor]

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

opaque Lean.noConfusionExt : TagDeclarationExtension

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

@[export lean_is_no_confusion]

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