Lean.AuxRecursor

source

def Lean.casesOnSuffix:

String

Equations

Lean.casesOnSuffix = "casesOn"

source

def Lean.recOnSuffix:

String

Equations

Lean.recOnSuffix = "recOn"

source

def Lean.brecOnSuffix:

String

Equations

Lean.brecOnSuffix = "brecOn"

source

def Lean.binductionOnSuffix:

String

Equations

Lean.binductionOnSuffix = "binductionOn"

source

def Lean.belowSuffix:

String

Equations

Lean.belowSuffix = "below"

source

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

Lean.Name

Equations

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

source

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

Lean.Name

Equations

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

source

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

Lean.Name

Equations

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

source

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

Lean.Name

Equations

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

source

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

Lean.Name

Equations

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

source

opaque Lean.auxRecExt:

Lean.TagDeclarationExtension

source

@[export lean_mark_aux_recursor]

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

Lean.Environment

Equations

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

source

@[export lean_is_aux_recursor]

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

Bool

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

opaque Lean.noConfusionExt:

Lean.TagDeclarationExtension

source

@[export lean_mark_no_confusion]

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

Lean.Environment

Equations

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

source

@[export lean_is_no_confusion]

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

Bool

Equations

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