Pantograph/Environment.lean

@@ -10,16 +10,12 @@ namespace Pantograph.Environment
 @[export pantograph_is_name_internal]
 def isNameInternal (n: Name): Bool :=
   -- 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 -/
 @[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
   | true => acc)
 
@@ -28,14 +24,6 @@ def module_of_name (env: Environment) (name: Name): Option Name := do
   let moduleId ←  env.getModuleIdxFor? name
   return env.allImportedModuleNames.get! moduleId.toNat
 
-@[export pantograph_constant_info_is_unsafe_or_partial]
-def constantInfoIsUnsafeOrPartial (info: ConstantInfo): Bool := info.isUnsafe || info.isPartial
-
-@[export pantograph_constant_info_type]
-def constantInfoType (info: ConstantInfo): CoreM Expr := unfoldAuxLemmas info.type
-@[export pantograph_constant_info_value]
-def constantInfoValue (info: ConstantInfo): CoreM (Option Expr) := info.value?.mapM unfoldAuxLemmas
-
 def toCompactSymbolName (n: Name) (info: ConstantInfo): String :=
   let pref := match info with
   | .axiomInfo  _ => "a"

Test/Environment.lean

@@ -33,7 +33,7 @@ def test_catalog: IO LSpec.TestSeq := do
 def test_symbol_visibility: IO LSpec.TestSeq := do
   let entries: List (Name × Bool) := [
     ("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),
   ]
   let suite := entries.foldl (λ suites (symbol, target) =>