chore: align isInternalName with upstream version (#796)

* chore: align isInternalName with upstream version * doc-string
leanprover-community · Jun 1, 2024 · dfe8208 · dfe8208
1 parent 60d622c
commit dfe8208
Showing 1 changed file with 7 additions and 2 deletions.
diff --git a/Batteries/Lean/Name.lean b/Batteries/Lean/Name.lean
@@ -16,8 +16,13 @@ Generally, user code should not explicitly use internal names.
 def isInternalDetail : Name → Bool
   | .str p s     =>
     s.startsWith "_"
-      || s.startsWith "match_"
-      || s.startsWith "proof_"
+      || matchPrefix s "eq_"
+      || matchPrefix s "match_"
+      || matchPrefix s "proof_"
       || p.isInternalOrNum
   | .num _ _     => true
   | p            => p.isInternalOrNum
+where
+  /-- Check that a string begins with the given prefix, and then is only digit characters. -/
+  matchPrefix (s : String) (pre : String) :=
+    s.startsWith pre && (s |>.drop pre.length |>.all Char.isDigit)