Skip to content

Commit 19556b4

Browse files
committed
fix breakage due to rebase
1 parent 5a97a78 commit 19556b4

File tree

1 file changed

+2
-3
lines changed
  • src/Std/Data/Iterators/Lemmas/Combinators

1 file changed

+2
-3
lines changed

src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,9 +25,8 @@ theorem Iter.step_drop {α β} [Iterator α Id β] {n : Nat}
2525
| k + 1 => .skip (it'.drop k) (.drop h rfl)
2626
| .skip it' h => .skip (it'.drop n) (.skip h)
2727
| .done h => .done (.done h)) := by
28-
simp only [Iter.step, Iter.step, Iter.drop_eq, IterM.step_drop, toIterM_toIter]
29-
simp only [Id.pure_eq, Id.bind_eq, Id.run, drop_eq]
30-
generalize it.toIterM.step = step
28+
simp only [drop_eq, step, toIterM_toIter, IterM.step_drop, Id.run_bind]
29+
generalize it.toIterM.step.run = step
3130
obtain ⟨step, h⟩ := step
3231
cases step <;> cases n <;>
3332
simp [PlausibleIterStep.yield, PlausibleIterStep.skip, PlausibleIterStep.done]

0 commit comments

Comments
 (0)