def Lean.casesOnSuffix : String

def Lean.recOnSuffix : String

def Lean.brecOnSuffix : String

def Lean.binductionOnSuffix : String

def Lean.belowSuffix : String

def Lean.mkCasesOnName (indDeclName : Lake.Name) : Lake.Name

def Lean.mkRecOnName (indDeclName : Lake.Name) : Lake.Name

def Lean.mkBRecOnName (indDeclName : Lake.Name) : Lake.Name

def Lean.mkBInductionOnName (indDeclName : Lake.Name) : Lake.Name

def Lean.mkBelowName (indDeclName : Lake.Name) : Lake.Name

opaque Lean.auxRecExt : Lean.TagDeclarationExtension

@[export lean_mark_aux_recursor]

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

@[export lean_is_aux_recursor]

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

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

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

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

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

opaque Lean.noConfusionExt : Lean.TagDeclarationExtension

@[export lean_mark_no_confusion]

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

@[export lean_is_no_confusion]

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