filter internal names

ammkrn · Mar 1, 2023 · 759e270 · 759e270
1 parent 70b2314
commit 759e270
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/Main.lean b/Main.lean
@@ -5,8 +5,10 @@ def main (args : List String) : IO Unit := do
   initSearchPath (← findSysroot)
   let (imports, constants) := args.span (· != "--")
   let imports := imports.map fun mod => { module := Syntax.decodeNameLit ("`" ++ mod) |>.get! }
-  let constants? := constants.tail?.map (·.map fun c => Syntax.decodeNameLit ("`" ++ c) |>.get!)
   let env ← importModules imports {}
+  let constants := match constants.tail? with
+    | some cs => cs.map fun c => Syntax.decodeNameLit ("`" ++ c) |>.get!
+    | none    => env.constants.toList.map Prod.fst |>.filter (!·.isInternal)
   M.run env do
-    for c in constants?.getD (env.constants.toList.map (·.1)) do
+    for c in constants do
       let _ ← dumpConstant c