Commit 2023-04-10 15:18 59c21a0f
View on Github →Feat: Port/Data.Seq.Seq (#3187)
Port of Data.Seq.Seq
following Mathlib3 refactor to avoid Seq
overload.
Down to two issues:
-
bind_ret
goes like Mathlib3 right up to the last line but doesn't close (I've tried the full Mathlib3simp
invocation to no avail. -
bind_assoc
has issues with singlematch
lines gumming up the works, which shoulddsimp
away but don't