fix: quote Name.anonymous

src/Init/Meta.lean

@@ -792,7 +792,7 @@ instance : Quote Substring := ⟨fun s => Syntax.mkCApp `String.toSubstring #[qu
 
 -- in contrast to `Name.toString`, we can, and want to be, precise here
 private def getEscapedNameParts? (acc : List String) : Name → Option (List String)
-  | Name.anonymous => return acc
+  | Name.anonymous => if acc.isEmpty then none else some acc
   | Name.str n s _ => do
     let s ← Name.escapePart s
     getEscapedNameParts? (s::acc) n