Compare commits

..

3 Commits

Author SHA1 Message Date
Leni Aniva 967e3dfb4f
feat: Remove | in symbol output 2023-11-27 09:54:41 -08:00
Leni Aniva 0a5a96275f
chore: Version bump to 0.2.9 2023-11-26 23:48:47 -08:00
Leni Aniva 7690272bfa
feat: Shorter symbol category 2023-11-26 22:14:58 -08:00
2 changed files with 10 additions and 10 deletions

View File

@ -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

View File

@ -1,5 +1,5 @@
namespace Pantograph
def version := "0.2.8"
def version := "0.2.9"
end Pantograph