feat: Expose _private names
This commit is contained in:
parent
a454aaf1d4
commit
07ade4c822
|
@ -4,7 +4,7 @@ namespace Pantograph
|
||||||
|
|
||||||
def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
|
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 == "Lean"
|
||||||
| _ => true
|
| _ => true
|
||||||
nameDeduce ∨ info.isUnsafe
|
nameDeduce ∨ info.isUnsafe
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue