Skip to content

Commit 219dc19

Browse files
committed
fix pipeline?
1 parent 7745cfc commit 219dc19

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/Std/Data/Iterators/Lemmas/Consumers.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.Consumers.Monadic
88
import Std.Data.Iterators.Lemmas.Consumers.Collect
9+
import Std.Data.Iterators.Lemmas.Consumers.Loop

0 commit comments

Comments
 (0)