From c80d7567b6eea9ad4b1d692a3d2c902e153293af Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 4 Dec 2023 23:36:09 -0800
Subject: [PATCH] feat: Expose _private names

---
 Pantograph/Symbol.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Pantograph/Symbol.lean b/Pantograph/Symbol.lean
index a473b98..07bbc2c 100644
--- a/Pantograph/Symbol.lean
+++ b/Pantograph/Symbol.lean
@@ -4,7 +4,7 @@ namespace Pantograph
 
 def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
   let nameDeduce: Bool := match n.getRoot with
-  | .str _ name => name.startsWith "_" ∨ name == "Lean"
+  | .str _ name => name == "Lean"
   | _ => true
   nameDeduce ∨ info.isUnsafe