feat: Shorter symbol category
This commit is contained in:
parent
7b59937853
commit
7690272bfa
|
@ -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 :=
|
||||
|
|
Loading…
Reference in New Issue