diff --git a/Pantograph/Symbol.lean b/Pantograph/Symbol.lean index fb0ea1d..3b781b5 100644 --- a/Pantograph/Symbol.lean +++ b/Pantograph/Symbol.lean @@ -14,14 +14,14 @@ def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String := let pref := match info with - | .axiomInfo _ => "axiom" - | .defnInfo _ => "defn" - | .thmInfo _ => "thm" - | .opaqueInfo _ => "opaque" - | .quotInfo _ => "quot" - | .inductInfo _ => "induct" - | .ctorInfo _ => "ctor" - | .recInfo _ => "rec" + | .axiomInfo _ => "a" + | .defnInfo _ => "d" + | .thmInfo _ => "t" + | .opaqueInfo _ => "o" + | .quotInfo _ => "q" + | .inductInfo _ => "i" + | .ctorInfo _ => "c" + | .recInfo _ => "r" s!"{pref}|{toString n}" def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=