From 3c90f512f6db453809b7634d2038e2403f71fe1f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 30 Aug 2024 10:41:35 +1000 Subject: [PATCH] implies --- ImportGraph/Cli.lean | 2 +- Main.lean | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index dca2763..0f9ff45 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -77,7 +77,7 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do let toModule := ImportGraph.getModule to let includeLean := args.hasFlag "include-lean" let includeStd := args.hasFlag "include-std" || includeLean - let includeDeps := args.hasFlag "include-deps" || includeStd + let includeDeps := args.hasFlag "include-deps" || args.hasFlag "mark-module" || includeStd let filter (n : Name) : Bool := toModule.isPrefixOf n || bif isPrefixOf `Std n then includeStd else diff --git a/Main.lean b/Main.lean index ddd910f..7e65269 100644 --- a/Main.lean +++ b/Main.lean @@ -21,9 +21,9 @@ 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 libraries (not including Lean itself and `std`)" - "mark-module"; "visually highlight the current module. Only sensible in combination with `--include-deps`" - "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')" + "mark-module"; "Visually highlight the current module. (implies `--include-deps`)" + "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. \