Skip to content

Commit 920f8c1

Browse files
committed
help orphaned modules
1 parent a944207 commit 920f8c1

File tree

4 files changed

+4
-0
lines changed

4 files changed

+4
-0
lines changed

src/Std/Data/Iterators/Combinators.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ Authors: Paul Reichert
66
prelude
77
import Std.Data.Iterators.Combinators.Monadic
88
import Std.Data.Iterators.Combinators.Take
9+
import Std.Data.Iterators.Combinators.Drop

src/Std/Data/Iterators/Combinators/Monadic.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,3 +5,4 @@ Authors: Paul Reichert
55
-/
66
prelude
77
import Std.Data.Iterators.Combinators.Monadic.Take
8+
import Std.Data.Iterators.Combinators.Monadic.Drop

src/Std/Data/Iterators/Lemmas/Combinators.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ Authors: Paul Reichert
66
prelude
77
import Std.Data.Iterators.Lemmas.Combinators.Monadic
88
import Std.Data.Iterators.Lemmas.Combinators.Take
9+
import Std.Data.Iterators.Lemmas.Combinators.Drop

src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,3 +5,4 @@ Authors: Paul Reichert
55
-/
66
prelude
77
import Std.Data.Iterators.Lemmas.Combinators.Monadic.Take
8+
import Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop

0 commit comments

Comments
 (0)