From e6954bb4f308406452f89bbb2ed2f064fc43b0f0 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 6 Apr 2022 15:23:35 +0200
Subject: [PATCH] fix: `quote Name.anonymous`

---
 src/Init/Meta.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index a5602fd505..8d5b23c0d2 100644
--- a/src/Init/Meta.lean
+++ b/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