From 6eff84a7bbc6e4e2da6cc017531451715fcd6671 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Sep 2021 16:30:09 -0700
Subject: [PATCH] refactor: add generic `mkBaseNameFor`

---
 src/Lean/Environment.lean         | 19 +++++++++++++++++++
 src/Lean/Meta/Match/MatchEqs.lean | 14 ++------------
 2 files changed, 21 insertions(+), 12 deletions(-)

diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 6653f9a483..e87f555bbb 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -780,4 +780,23 @@ instance (m n) [MonadLift m n] [MonadEnv m] : MonadEnv n where
   getEnv    := liftM (getEnv : m Environment)
   modifyEnv := fun f => liftM (modifyEnv f : m Unit)
 
+/--
+  If `env` does not contain a declaration with name `declName ++ elemSuffix`, then return `declName`.
+  Otherwise, find the smallest positive `Nat` `i` such that `declName ++ suffix.appendIndexAfter i ++ elemSuffix` is not
+  the name of a declaration in the given environment.
+-/
+partial def mkBaseNameFor (env : Environment) (declName : Name) (elemSuffix : Name) (suffix : Name) : Name :=
+  if !env.contains (declName ++ elemSuffix) then
+    declName
+  else
+    go 1
+where
+  go (idx : Nat) : Name :=
+    let baseName := declName ++ suffix.appendIndexAfter idx
+    if !env.contains (baseName ++ elemSuffix) then
+      baseName
+    else
+      go (idx + 1)
+
+
 end Lean
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index 795c78d493..faaaaee3e7 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -28,18 +28,8 @@ private def registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : C
   modifyEnv fun env => matchEqnsExt.modifyState env fun s => { s with map := s.map.insert matchDeclName matchEqns }
 
 /-- Create a "unique" base name for conditional equations and splitter -/
-private partial def mkBaseNameFor (env : Environment) (matchDeclName : Name) : Name :=
-  if !env.contains (matchDeclName ++ `splitter) then
-    matchDeclName
-  else
-   go 1
-where
-  go (idx : Nat) : Name :=
-    let baseName := matchDeclName ++ (`_matchEqns).appendIndexAfter idx
-    if !env.contains (baseName ++ `splitter) then
-      baseName
-    else
-      go (idx + 1)
+private def mkBaseNameFor (env : Environment) (matchDeclName : Name) : Name :=
+  Lean.mkBaseNameFor env matchDeclName `splitter `_matchEqns
 
 /--
   Helper method. Recall that alternatives that do not have variables have a `Unit` parameter to ensure