Skip to content

Commit c4dc8c7

Browse files
committed
Fix imports
1 parent a7b5efc commit c4dc8c7

File tree

2 files changed

+3
-1
lines changed

2 files changed

+3
-1
lines changed

src/Std/Data/DTreeMap.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,5 @@ prelude
99
public import Std.Data.DTreeMap.Basic
1010
public import Std.Data.DTreeMap.AdditionalOperations
1111
public import Std.Data.DTreeMap.Lemmas
12+
public import Std.Data.DTreeMap.Iterator
13+
public import Std.Data.DTreeMap.Slice

src/Std/Data/DTreeMap/Raw/Iterator.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ module
77

88
prelude
99
public import Std.Data.DTreeMap.Internal.Zipper
10-
public import Std.Data.DTreeMap
10+
public import Std.Data.DTreeMap.Raw.Basic
1111

1212
/-!
1313
# Iterators on `DTreeMap.Raw`

0 commit comments

Comments
 (0)