We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 881a874 commit ec20d61Copy full SHA for ec20d61
src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean
@@ -33,10 +33,10 @@ theorem ListIterator.toArrayMapped_eq [LawfulMonad m]
33
rw [LawfulIteratorCollect.toArrayMapped_eq]
34
induction l with
35
| nil =>
36
- rw [IterM.DefaultConsumers.toArrayMapped_of_step]
+ rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
37
simp [List.step_iterM_nil]
38
| cons x xs ih =>
39
40
simp [List.step_iterM_cons, List.mapM_cons, pure_bind, ih]
41
42
theorem _root_.List.toArray_iterM [LawfulMonad m] {l : List β} :
0 commit comments