chore: Version 0.3 #136
|
@ -6,11 +6,7 @@ def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool
|
||||||
let nameDeduce: Bool := match n.getRoot with
|
let nameDeduce: Bool := match n.getRoot with
|
||||||
| .str _ name => name.startsWith "_" ∨ name == "Lean"
|
| .str _ name => name.startsWith "_" ∨ name == "Lean"
|
||||||
| _ => true
|
| _ => true
|
||||||
let stemDeduce: Bool := match n with
|
nameDeduce ∨ info.isUnsafe
|
||||||
| .anonymous => true
|
|
||||||
| .str _ name => name.startsWith "_"
|
|
||||||
| .num _ _ => true
|
|
||||||
nameDeduce ∨ stemDeduce ∨ info.isUnsafe
|
|
||||||
|
|
||||||
def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
|
def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
|
||||||
let pref := match info with
|
let pref := match info with
|
||||||
|
|
Loading…
Reference in New Issue