feat: Remove | in symbol output

2023-11-27 09:54:41 -08:00 · 2023-11-27 09:54:41 -08:00 · 967e3dfb4f
parent 0a5a96275f
commit 967e3dfb4f
1 changed files with 1 additions and 1 deletions
--- 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