Skip to content

Commit c1514c2

Browse files
committed
correct docstrings
1 parent 8e81d8c commit c1514c2

File tree

1 file changed

+4
-8
lines changed

1 file changed

+4
-8
lines changed

src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -73,8 +73,7 @@ iterators are productive *and provably never empty*, then the resulting iterator
7373
This combinator incurs an additional O(1) cost with each output of `it₁`, `it₂` or an internal
7474
iterator.
7575
76-
For each value emitted by the outer iterator `it₁`, this combinator calls `f` and matches on the
77-
returned `Option` value.
76+
For each value emitted by the outer iterator `it₁`, this combinator calls `f`.
7877
-/
7978
@[always_inline]
8079
public def IterM.flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type w}
@@ -113,8 +112,7 @@ iterators are productive *and provably never empty*, then the resulting iterator
113112
114113
This combinator incurs an additional O(1) cost with each output of `it` or an internal iterator.
115114
116-
For each value emitted by the outer iterator `it`, this combinator calls `f` and matches on the
117-
returned `Option` value.
115+
For each value emitted by the outer iterator `it`, this combinator calls `f`.
118116
-/
119117
@[always_inline, expose]
120118
public def IterM.flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
@@ -156,8 +154,7 @@ iterators are productive *and provably never empty*, then the resulting iterator
156154
This combinator incurs an additional O(1) cost with each output of `it₁`, `it₂` or an internal
157155
iterator.
158156
159-
For each value emitted by the outer iterator `it₁`, this combinator calls `f` and matches on the
160-
returned `Option` value.
157+
For each value emitted by the outer iterator `it₁`, this combinator calls `f`.
161158
-/
162159
@[always_inline]
163160
public def IterM.flatMapAfter {α : Type w} {β : Type w} {α₂ : Type w}
@@ -196,8 +193,7 @@ iterators are productive *and provably never empty*, then the resulting iterator
196193
197194
This combinator incurs an additional O(1) cost with each output of `it` or an internal iterator.
198195
199-
For each value emitted by the outer iterator `it`, this combinator calls `f` and matches on the
200-
returned `Option` value.
196+
For each value emitted by the outer iterator `it`, this combinator calls `f`.
201197
-/
202198
@[always_inline, expose]
203199
public def IterM.flatMap {α : Type w} {β : Type w} {α₂ : Type w}

0 commit comments

Comments
 (0)