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

Equations

• Lean.ibelowSuffix = "ibelow"

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.mkIBelowName indDeclName = indDeclName.mkStr Lean.ibelowSuffix

opaque Lean.auxRecExt : Lean.TagDeclarationExtension

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

Equations

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

@[export lean_is_aux_recursor]

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

Equations

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

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

Equations

• Lean.isAuxRecursorWithSuffix env declName suffix = match declName with | pre.str s => 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.casesOnSuffix

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

Equations

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

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

Equations

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

opaque Lean.noConfusionExt : Lean.TagDeclarationExtension

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

Equations

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

@[export lean_is_no_confusion]

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

Equations

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