From 967e3dfb4f2aa808250967d43a8be25965537c0d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 27 Nov 2023 09:54:41 -0800
Subject: [PATCH] feat: Remove | in symbol output

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

diff --git a/Pantograph/Symbol.lean b/Pantograph/Symbol.lean
index 3b781b5..5fbb0d0 100644
--- a/Pantograph/Symbol.lean
+++ b/Pantograph/Symbol.lean
@@ -22,7 +22,7 @@ def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
   | .inductInfo _ => "i"
   | .ctorInfo   _ => "c"
   | .recInfo    _ => "r"
-  s!"{pref}|{toString n}"
+  s!"{pref}{toString n}"
 
 def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
   if is_symbol_unsafe_or_internal n info