From 98453c468bf7445f09fc0e29d46f0daeac86e150 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 17 Sep 2020 16:30:03 +0200
Subject: [PATCH] feat: formatter: don't escape inaccessible names

---
 src/Lean/PrettyPrinter/Formatter.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 4f6364acef..16fa629397 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -266,7 +266,7 @@ let id := stx.getId;
 let s := id.toString;
 if id.isAnonymous then
   pushToken "[anonymous]"
-else if id.components.any Name.isNum then
+else if LocalContext.isInaccessibleUserName id || id.components.any Name.isNum then
   -- not parsable anyway, output as-is
   pushToken s
 else do {