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.binductionOnSuffix : String

Equations

• Lean.binductionOnSuffix = "binductionOn"

def Lean.belowSuffix : String

Equations

• Lean.belowSuffix = "below"

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.mkBInductionOnName indDeclName = Lean.Name.mkStr indDeclName Lean.binductionOnSuffix

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

Equations

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

opaque Lean.auxRecExt : Lean.TagDeclarationExtension

@[export lean_mark_aux_recursor]

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

Equations

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

@[export lean_is_aux_recursor]

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

Equations

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

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

Equations

• Lean.isAuxRecursorWithSuffix env declName suffix = match declName with | Lean.Name.str pre s => Lean.Name.mkSimple s == suffix && Lean.isAuxRecursor env declName | x => false

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

Equations

• Lean.isCasesOnRecursor env declName = Lean.isAuxRecursorWithSuffix env declName (Lean.Name.mkSimple Lean.casesOnSuffix)

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

Equations

• Lean.isRecOnRecursor env declName = Lean.isAuxRecursorWithSuffix env declName (Lean.Name.mkSimple Lean.recOnSuffix)

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

Equations

• Lean.isBRecOnRecursor env declName = Lean.isAuxRecursorWithSuffix env declName (Lean.Name.mkSimple Lean.brecOnSuffix)

opaque Lean.noConfusionExt : Lean.TagDeclarationExtension

@[export lean_mark_no_confusion]

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

Equations

• Lean.markNoConfusion env n = Lean.TagDeclarationExtension.tag Lean.noConfusionExt env n

@[export lean_is_no_confusion]

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

Equations

• Lean.isNoConfusion env n = Lean.TagDeclarationExtension.isTagged Lean.noConfusionExt env n