From e8cd32ff240b625de7f9d18084bba90aed97002f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Sep 2021 18:37:29 -0700 Subject: [PATCH] chore: add `mkBelowName` --- src/Lean/AuxRecursor.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Lean/AuxRecursor.lean b/src/Lean/AuxRecursor.lean index 3419c43042..de557215e9 100644 --- a/src/Lean/AuxRecursor.lean +++ b/src/Lean/AuxRecursor.lean @@ -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