add comment

leanprover · Aug 27, 2024 · 362f60c · 362f60c
1 parent b785fae
commit 362f60c
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
@@ -115,6 +115,8 @@ def getRoot : Name → Name
 
 @[export lean_is_inaccessible_user_name]
 def isInaccessibleUserName : Name → Bool
+  -- note: this uses `✝` (`\u{271D}`) whereas everywhere else in the code
+  -- we use the text-variant selector `✝︎` (`\u{271D}\u{FE0E}`).
   | Name.str _ s   => s.contains '✝' || s == "_inaccessible"
   | Name.num p _   => isInaccessibleUserName p
   | _              => false