better logic

leanprover-community · Aug 29, 2024 · d8b01ef · d8b01ef
1 parent 97c056c
commit d8b01ef
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean
@@ -41,8 +41,8 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
       graph := graph.downstreamOf (NameSet.empty.insert f)
     let toModule := ImportGraph.getModule to
     let includeLean := args.hasFlag "include-lean"
-    let includeStd := args.hasFlag "include-std"
-    let includeDeps := args.hasFlag "include-deps"
+    let includeStd := args.hasFlag "include-std" || includeLean
+    let includeDeps := args.hasFlag "include-deps" || includeStd
     let filter (n : Name) : Bool :=
       toModule.isPrefixOf n ||
       bif isPrefixOf `Std n then includeStd else

diff --git a/Main.lean b/Main.lean
@@ -21,8 +21,8 @@ def graph : Cmd := `[Cli|
     "from" : ModuleName;  "Only show the downstream dependencies of the specified module."
     "exclude-meta";       "Exclude any files starting with `Mathlib.[Tactic|Lean|Util|Mathport]`."
     "include-deps";       "Include used files from other projects (e.g. lake packages)"
-    "include-std";        "Include used files from the Lean standard library"
-    "include-lean";       "Include used files from Lean itself (`Lean.*` and `Init.*`)"
+    "include-std";        "Include used files from the Lean standard library (implies 'include-deps')"
+    "include-lean";       "Include used files from Lean itself (implies 'include-deps' and 'include-std')"
 
   ARGS:
     ...outputs : String;  "Filename(s) for the output. \