feat: Remove most filters on catalog
This commit is contained in:
parent
b174b4ea79
commit
3c808506c1
|
@ -10,16 +10,12 @@ namespace Pantograph.Environment
|
||||||
@[export pantograph_is_name_internal]
|
@[export pantograph_is_name_internal]
|
||||||
def isNameInternal (n: Name): Bool :=
|
def isNameInternal (n: Name): Bool :=
|
||||||
-- Returns true if the name is an implementation detail which should not be shown to the user.
|
-- Returns true if the name is an implementation detail which should not be shown to the user.
|
||||||
isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ n.isAuxLemma ∨ n.hasMacroScopes
|
n.isAuxLemma ∨ n.hasMacroScopes
|
||||||
where
|
|
||||||
isLeanSymbol (name: Name): Bool := match name.getRoot with
|
|
||||||
| .str _ name => name == "Lean"
|
|
||||||
| _ => true
|
|
||||||
|
|
||||||
/-- Catalog all the non-internal and safe names -/
|
/-- Catalog all the non-internal and safe names -/
|
||||||
@[export pantograph_environment_catalog]
|
@[export pantograph_environment_catalog]
|
||||||
def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name info =>
|
def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name _ =>
|
||||||
match isNameInternal name || info.isUnsafe with
|
match isNameInternal name with
|
||||||
| false => acc.push name
|
| false => acc.push name
|
||||||
| true => acc)
|
| true => acc)
|
||||||
|
|
||||||
|
|
|
@ -33,7 +33,7 @@ def test_catalog: IO LSpec.TestSeq := do
|
||||||
def test_symbol_visibility: IO LSpec.TestSeq := do
|
def test_symbol_visibility: IO LSpec.TestSeq := do
|
||||||
let entries: List (Name × Bool) := [
|
let entries: List (Name × Bool) := [
|
||||||
("Nat.add_comm".toName, false),
|
("Nat.add_comm".toName, false),
|
||||||
("Lean.Name".toName, true),
|
("foo.bla.Init.Data.List.Basic.2.1.Init.Lean.Expr._hyg.4".toName, true),
|
||||||
("Init.Data.Nat.Basic._auxLemma.4".toName, true),
|
("Init.Data.Nat.Basic._auxLemma.4".toName, true),
|
||||||
]
|
]
|
||||||
let suite := entries.foldl (λ suites (symbol, target) =>
|
let suite := entries.foldl (λ suites (symbol, target) =>
|
||||||
|
|
Loading…
Reference in New Issue