Skip to content

Commit

Permalink
Update ImportGraph/RequiredModules.lean
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em authored Aug 29, 2024
1 parent fedbcef commit 64a9dd8
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion ImportGraph/RequiredModules.lean
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ def Name.transitivelyRequiredModules (n : Name) (env : Environment) : CoreM Name

/--
Finds all constants defined in the specified module,
and identifies all modules contains constants which are transitively required by those constants.
and identifies all modules containing constants which are transitively required by those constants.
-/
def Environment.transitivelyRequiredModules (env : Environment) (module : Name) : CoreM NameSet := do
let mut requiredModules : NameSet := {}
Expand Down

0 comments on commit 64a9dd8

Please sign in to comment.