Skip to content

Commit

Permalink
No longer needed dsimps?
Browse files Browse the repository at this point in the history
  • Loading branch information
nomeata committed Aug 16, 2024
1 parent 2298410 commit 66ff376
Showing 1 changed file with 0 additions and 2 deletions.
2 changes: 0 additions & 2 deletions Mathlib/Data/Seq/Parallel.lean
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,6 @@ theorem terminates_parallel {S : WSeq (Computation α)} {c} (h : c ∈ S) [T : T
· have C : corec parallel.aux1 (l, S) = pure a := by
apply destruct_eq_pure
rw [corec_eq, parallel.aux1]
dsimp only []
rw [h]
simp only [rmap]
rw [C]
Expand All @@ -146,7 +145,6 @@ theorem terminates_parallel {S : WSeq (Computation α)} {c} (h : c ∈ S) [T : T
· have C : corec parallel.aux1 (l, S) = pure a := by
apply destruct_eq_pure
rw [corec_eq, parallel.aux1]
dsimp only []
rw [h]
simp only [rmap]
rw [C]
Expand Down

0 comments on commit 66ff376

Please sign in to comment.