Documentation

Lean.AuxRecursor

def Lean.casesOnSuffix :

Equations

Lean.casesOnSuffix = "casesOn"

def Lean.recOnSuffix :

Equations

Lean.recOnSuffix = "recOn"

def Lean.brecOnSuffix :

Equations

Lean.brecOnSuffix = "brecOn"

def Lean.binductionOnSuffix :

Equations

Lean.binductionOnSuffix = "binductionOn"

def Lean.belowSuffix :

Equations

Lean.belowSuffix = "below"

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

constant Lean.auxRecExt :

Lean.TagDeclarationExtension

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

Lean.Environment

Equations

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

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

Equations

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

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

Equations

Lean.isCasesOnRecursor env declName = match declName with | Lean.Name.str x s x_1 => s == Lean.casesOnSuffix && Lean.isAuxRecursor env declName | x => false

constant Lean.noConfusionExt :

Lean.TagDeclarationExtension

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

Lean.Environment

Equations

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

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

Equations

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