refactor: add generic mkBaseNameFor

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

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