From a454aaf1d44af364a8eb9d9366625f49f3bb9fe2 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 4 Dec 2023 16:40:15 -0800
Subject: [PATCH] feat: Remove stem deduce

Some private subproofs are not shown in the catalog and this breaks
dependencies
---
 Pantograph/Symbol.lean | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/Pantograph/Symbol.lean b/Pantograph/Symbol.lean
index 5fbb0d0..a473b98 100644
--- a/Pantograph/Symbol.lean
+++ b/Pantograph/Symbol.lean
@@ -6,11 +6,7 @@ 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"
   | _ => true
-  let stemDeduce: Bool := match n with
-  | .anonymous => true
-  | .str _ name => name.startsWith "_"
-  | .num _ _ => true
-  nameDeduce ∨ stemDeduce ∨ info.isUnsafe
+  nameDeduce ∨ info.isUnsafe
 
 def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
   let pref := match info with