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