Skip to content

Commit 4df3d9b

Browse files
committed
add imports
1 parent 2377097 commit 4df3d9b

File tree

3 files changed

+16
-0
lines changed

3 files changed

+16
-0
lines changed

src/Std/Data/Iterators/Lemmas.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,3 +7,4 @@ prelude
77
import Std.Data.Iterators.Lemmas.Basic
88
import Std.Data.Iterators.Lemmas.Monadic
99
import Std.Data.Iterators.Lemmas.Consumers
10+
import Std.Data.Iterators.Lemmas.Producers
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
/-
2+
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Paul Reichert
5+
-/
6+
prelude
7+
import Std.Data.Iterators.Lemmas.Producers.Monadic
8+
import Std.Data.Iterators.Lemmas.Producers.List
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
/-
2+
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Paul Reichert
5+
-/
6+
prelude
7+
import Std.Data.Iterators.Lemmas.Producers.Monadic.List

0 commit comments

Comments
 (0)