Skip to content

Commit

Permalink
Feat: Port/Data.Seq.Seq (#3187)
Browse files Browse the repository at this point in the history
Port of `Data.Seq.Seq` following Mathlib3 refactor to avoid `Seq` overload.

Down to two issues:

- [x] `bind_ret` goes like Mathlib3 right up to the last line but doesn't close (I've tried the full Mathlib3 `simp` invocation to no avail.
- [x] `bind_assoc` has issues with single `match` lines gumming up the works, which should `dsimp` away but don't




Co-authored-by: Komyyy <pol_tta@outlook.jp>
  • Loading branch information
arienmalec and Komyyy committed Apr 10, 2023
1 parent 16371bd commit 59c21a0
Show file tree
Hide file tree
Showing 2 changed files with 1,072 additions and 0 deletions.
1 change: 1 addition & 0 deletions Mathlib.lean
Expand Up @@ -989,6 +989,7 @@ import Mathlib.Data.Real.Sqrt
import Mathlib.Data.Rel
import Mathlib.Data.Semiquot
import Mathlib.Data.Seq.Computation
import Mathlib.Data.Seq.Seq
import Mathlib.Data.Set.Accumulate
import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.BoolIndicator
Expand Down

0 comments on commit 59c21a0

Please sign in to comment.