max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add mkBelowName

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-18 18:37:29 -07:00
parent 2775298fef
commit e8cd32ff24
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/AuxRecursor.lean
View file

@ -11,11 +11,13 @@ def casesOnSuffix := "casesOn"
def recOnSuffix := "recOn"
def brecOnSuffix := "brecOn"
def binductionOnSuffix := "binductionOn"
def belowSuffix := "below"
def mkCasesOnName (indDeclName : Name) : Name := Name.mkStr indDeclName casesOnSuffix
def mkRecOnName (indDeclName : Name) : Name := Name.mkStr indDeclName recOnSuffix
def mkBRecOnName (indDeclName : Name) : Name := Name.mkStr indDeclName brecOnSuffix
def mkBInductionOnName (indDeclName : Name) : Name := Name.mkStr indDeclName binductionOnSuffix
def mkBelowName (indDeclName : Name) : Name := Name.mkStr indDeclName belowSuffix
builtin_initialize auxRecExt : TagDeclarationExtension ← mkTagDeclarationExtension `auxRec