fix: unorphan modules in Std.Data

leanprover · Jul 8, 2024 · 76a2a3c · 76a2a3c
1 parent 6ed26dc
commit 76a2a3c
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/src/Std/Data.lean b/src/Std/Data.lean
@@ -7,3 +7,10 @@ prelude
 import Std.Data.DHashMap
 import Std.Data.HashMap
 import Std.Data.HashSet
+
+-- The three imports above only import the modules needed to work with the version which bundles
+-- the well-formedness invariant, so we need to additionally import the files that deal with the
+-- unbundled version
+import Std.Data.DHashMap.RawLemmas
+import Std.Data.HashMap.RawLemmas
+import Std.Data.HashSet.RawLemmas
diff --git a/src/Std/Data/DHashMap.lean b/src/Std/Data/DHashMap.lean
@@ -5,6 +5,5 @@ Authors: Markus Himmel
 -/
 prelude
 import Std.Data.DHashMap.Basic
-import Std.Data.DHashMap.RawLemmas
 import Std.Data.DHashMap.Lemmas
 import Std.Data.DHashMap.AdditionalOperations