From 472276f63f4f40a1015ffdfae95a0efe034f6d6b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 22 Feb 2020 11:24:46 -0800
Subject: [PATCH] feat: add `mkRecFor`

---
 src/Init/Lean/Declaration.lean       | 4 ++++
 src/Init/Lean/Meta/RecursorInfo.lean | 2 +-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Declaration.lean b/src/Init/Lean/Declaration.lean
index 4f8b67929d..edaf91d4a3 100644
--- a/src/Init/Lean/Declaration.lean
+++ b/src/Init/Lean/Declaration.lean
@@ -213,4 +213,8 @@ constant instantiateTypeLevelParams (c : @& ConstantInfo) (ls : @& List Level) :
 constant instantiateValueLevelParams (c : @& ConstantInfo) (ls : @& List Level) : Expr := arbitrary _
 
 end ConstantInfo
+
+def mkRecFor (declName : Name) : Name :=
+mkNameStr declName "rec"
+
 end Lean
diff --git a/src/Init/Lean/Meta/RecursorInfo.lean b/src/Init/Lean/Meta/RecursorInfo.lean
index 217c8d2476..c073affe1e 100644
--- a/src/Init/Lean/Meta/RecursorInfo.lean
+++ b/src/Init/Lean/Meta/RecursorInfo.lean
@@ -106,7 +106,7 @@ else do
     if s != "recOn" && s != "casesOn" && s != "brecOn" then
       pure none
     else do
-      recInfo ← getConstInfo (mkNameStr p "rec");
+      recInfo ← getConstInfo (mkRecFor p);
       match recInfo with
       | ConstantInfo.recInfo val => pure (some (val.nparams + val.nindices + (if s == "casesOn" then 1 else val.nmotives)))
       | _                        => throw $ Exception.other "unexpected recursor information"