DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update check_file_imports.lean

Browse source
This commit is contained in:
jstoobysmith 2024-10-03 13:58:48 +00:00
parent 987bbf6013
commit 03bc9f3cd2
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
scripts/check_file_imports.lean
View file

@ -66,7 +66,7 @@ def arrayImportSorted (imports : Array Import) : IO Bool := do
return true if this is NOT the case. -/
def checkMissingImports (modData : ModuleData) (reqImports : Array Name) :
IO Bool := do
let names : HashSet Name := HashSet.ofArray (modData.imports.map (·.module))
let names : Std.HashSet Name := Std.HashSet.ofArray (modData.imports.map (·.module))
let mut warned := false
let nameArray := reqImports.filterMap (
fun req => if !names.contains req then