feat: Remove stem deduce
Some private subproofs are not shown in the catalog and this breaks dependencies
This commit is contained in:
parent
967e3dfb4f
commit
a454aaf1d4
|
@ -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