Commit 2025-03-31 04:41 01dba5e8

View on Github →

chore: split Data.WSeq.Basic (#23294)

  • Data.WSeq.Basic contains basic definitions and lemmas.
  • Data.WSeq.Defs contains definitions not used anywhere else.
  • Data.WSeq.Productive contains the Productive property and toSeq. They too are not used anywhere else.
  • Data.WSeq.Relation defines relations and equivalence on weak sequences. This file is needed by Data.Seq.Parallel.

Estimated changes

deleted theorem Stream'.WSeq.BisimO.imp
deleted def Stream'.WSeq.BisimO
deleted theorem Stream'.WSeq.Equiv.ext
deleted theorem Stream'.WSeq.Equiv.refl
deleted theorem Stream'.WSeq.Equiv.symm
deleted theorem Stream'.WSeq.Equiv.trans
deleted def Stream'.WSeq.Equiv
deleted theorem Stream'.WSeq.LiftRel.refl
deleted theorem Stream'.WSeq.LiftRel.swap
deleted theorem Stream'.WSeq.LiftRel.symm
deleted theorem Stream'.WSeq.LiftRelO.imp
deleted def Stream'.WSeq.all
deleted def Stream'.WSeq.any
deleted theorem Stream'.WSeq.bind_assoc
deleted theorem Stream'.WSeq.bind_congr
deleted theorem Stream'.WSeq.bind_ret
deleted theorem Stream'.WSeq.cons_congr
deleted theorem Stream'.WSeq.dropn_congr
deleted def Stream'.WSeq.filter
deleted def Stream'.WSeq.find
deleted def Stream'.WSeq.get
deleted theorem Stream'.WSeq.get?_congr
deleted theorem Stream'.WSeq.head_congr
deleted def Stream'.WSeq.inits
deleted theorem Stream'.WSeq.join_append
deleted theorem Stream'.WSeq.join_congr
deleted theorem Stream'.WSeq.join_join
deleted theorem Stream'.WSeq.join_map_ret
deleted theorem Stream'.WSeq.join_ret
deleted def Stream'.WSeq.length
deleted theorem Stream'.WSeq.liftRel_bind
deleted theorem Stream'.WSeq.liftRel_cons
deleted theorem Stream'.WSeq.liftRel_join
deleted theorem Stream'.WSeq.liftRel_map
deleted theorem Stream'.WSeq.liftRel_nil
deleted theorem Stream'.WSeq.map_congr
deleted theorem Stream'.WSeq.mem_congr
deleted theorem Stream'.WSeq.ret_bind
deleted def Stream'.WSeq.scanl
deleted theorem Stream'.WSeq.tail_congr
deleted def Stream'.WSeq.take
deleted theorem Stream'.WSeq.think_congr
deleted theorem Stream'.WSeq.think_equiv
deleted def Stream'.WSeq.toSeq
deleted theorem Stream'.WSeq.toSeq_ofSeq
deleted def Stream'.WSeq.union
deleted def Stream'.WSeq.zip
added def Stream'.WSeq.all
added def Stream'.WSeq.any
added def Stream'.WSeq.get
added def Stream'.WSeq.zip
added theorem Stream'.WSeq.Equiv.ext
added theorem Stream'.WSeq.bind_ret
added theorem Stream'.WSeq.join_join
added theorem Stream'.WSeq.join_ret
added theorem Stream'.WSeq.map_congr
added theorem Stream'.WSeq.mem_congr
added theorem Stream'.WSeq.ret_bind