From 83383b505f26f4e2b2f012690c2923e60f4093d7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Mar 2020 09:49:00 -0800 Subject: [PATCH] chore: auxiliary functions --- src/Init/Lean/Meta/RecursorInfo.lean | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/Init/Lean/Meta/RecursorInfo.lean b/src/Init/Lean/Meta/RecursorInfo.lean index a94401f322..297e119216 100644 --- a/src/Init/Lean/Meta/RecursorInfo.lean +++ b/src/Init/Lean/Meta/RecursorInfo.lean @@ -13,6 +13,14 @@ import Init.Lean.Meta.Message namespace Lean namespace Meta +def casesOnSuffix := "casesOn" +def recOnSuffix := "recOn" +def brecOnSuffix := "brecOn" + +def mkCasesOnFor (indDeclName : Name) : Name := mkNameStr indDeclName casesOnSuffix +def mkRecOnFor (indDeclName : Name) : Name := mkNameStr indDeclName recOnSuffix +def mkBRecOnFor (indDeclName : Name) : Name := mkNameStr indDeclName brecOnSuffix + inductive RecursorUnivLevelPos | motive -- marks where the universe of the motive should go | majorType (idx : Nat) -- marks where the #idx universe of the major premise type goes @@ -104,12 +112,12 @@ else do if !isAuxRecursor env declName then pure none else match declName with | Name.str p s _ => - if s != "recOn" && s != "casesOn" && s != "brecOn" then + if s != recOnSuffix && s != casesOnSuffix && s != brecOnSuffix then pure none else do recInfo ← getConstInfo (mkRecFor p); match recInfo with - | ConstantInfo.recInfo val => pure (some (val.nparams + val.nindices + (if s == "casesOn" then 1 else val.nmotives))) + | ConstantInfo.recInfo val => pure (some (val.nparams + val.nindices + (if s == casesOnSuffix then 1 else val.nmotives))) | _ => throw $ Exception.other "unexpected recursor information" | _ => pure none