Skip to content

Commit 2ec8a83

Browse files
datokratdatokrat
committed
fix pipeline?
1 parent 5d96ec0 commit 2ec8a83

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)