feat: Shorter symbol category #33
|
@ -14,15 +14,15 @@ 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"
|
||||
s!"{pref}|{toString n}"
|
||||
| .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 :=
|
||||
if is_symbol_unsafe_or_internal n info
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
namespace Pantograph
|
||||
|
||||
def version := "0.2.8"
|
||||
def version := "0.2.9"
|
||||
|
||||
end Pantograph
|
||||
|
|
Loading…
Reference in New Issue