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 Mathlib3 simp invocation to no avail.
  • bind_assoc has issues with single match lines gumming up the works, which should dsimp away but don't

Estimated changes

added def Stream'.IsSeq
added theorem Stream'.Seq.append_nil
added def Stream'.Seq.cons
added theorem Stream'.Seq.corec_eq
added def Stream'.Seq.drop
added theorem Stream'.Seq.dropn_add
added theorem Stream'.Seq.dropn_tail
added def Stream'.Seq.enum
added theorem Stream'.Seq.enum_cons
added theorem Stream'.Seq.enum_nil
added theorem Stream'.Seq.ge_stable
added def Stream'.Seq.get?
added theorem Stream'.Seq.get?_enum
added theorem Stream'.Seq.get?_mk
added theorem Stream'.Seq.get?_tail
added theorem Stream'.Seq.get?_zip
added def Stream'.Seq.head
added theorem Stream'.Seq.head_cons
added theorem Stream'.Seq.head_dropn
added theorem Stream'.Seq.head_nil
added def Stream'.Seq.join
added theorem Stream'.Seq.join_cons
added theorem Stream'.Seq.join_nil
added theorem Stream'.Seq.le_stable
added def Stream'.Seq.map
added theorem Stream'.Seq.map_append
added theorem Stream'.Seq.map_comp
added theorem Stream'.Seq.map_cons
added theorem Stream'.Seq.map_get?
added theorem Stream'.Seq.map_id
added theorem Stream'.Seq.map_nil
added theorem Stream'.Seq.map_tail
added theorem Stream'.Seq.mem_cons
added theorem Stream'.Seq.mem_map
added theorem Stream'.Seq.mem_rec_on
added def Stream'.Seq.nats
added theorem Stream'.Seq.nats_nth
added def Stream'.Seq.nil
added theorem Stream'.Seq.nil_append
added theorem Stream'.Seq.nth_nil
added theorem Stream'.Seq.ofList_nil
added theorem Stream'.Seq.ofList_nth
added def Stream'.Seq.omap
added def Stream'.Seq.tail
added theorem Stream'.Seq.tail_cons
added theorem Stream'.Seq.tail_nil
added def Stream'.Seq.take
added theorem Stream'.Seq.val_cons
added def Stream'.Seq.zip
added theorem Stream'.Seq1.bind_ret
added theorem Stream'.Seq1.join_cons
added theorem Stream'.Seq1.join_join
added theorem Stream'.Seq1.join_nil
added def Stream'.Seq1.map
added theorem Stream'.Seq1.map_id
added theorem Stream'.Seq1.map_join'
added theorem Stream'.Seq1.map_join
added theorem Stream'.Seq1.map_pair
added def Stream'.Seq1.ret
added theorem Stream'.Seq1.ret_bind
added def Stream'.Seq1
added def Stream'.Seq