aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

feat: Expose _private names

This commit is contained in:
Leni Aniva 2023-12-04 23:36:09 -08:00
parent f72a82a4c9
commit c80d7567b6
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Pantograph/Symbol.lean
View File

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