Commit 2023-01-23 20:28 382737dc

View on Github →

feat: port Data.Seq.Computation (#1216) Port of data.seq.computation Requires renaming return to pure

Estimated changes

added theorem Computation.Equiv.refl
added theorem Computation.Equiv.symm
added def Computation.bind
added theorem Computation.bind_assoc
added theorem Computation.bind_congr
added theorem Computation.bind_pure'
added theorem Computation.bind_pure
added theorem Computation.corec_eq
added theorem Computation.eq_thinkN'
added theorem Computation.eq_thinkN
added def Computation.get
added theorem Computation.get_bind
added theorem Computation.get_equiv
added theorem Computation.get_mem
added theorem Computation.get_pure
added theorem Computation.get_think
added theorem Computation.get_thinkN
added def Computation.head
added theorem Computation.head_empty
added theorem Computation.head_pure
added theorem Computation.head_think
added def Computation.join
added theorem Computation.le_stable
added def Computation.lmap
added def Computation.map
added theorem Computation.map_comp
added theorem Computation.map_congr
added theorem Computation.map_id
added theorem Computation.map_pure'
added theorem Computation.map_pure
added theorem Computation.map_think'
added theorem Computation.map_think
added theorem Computation.mem_bind
added theorem Computation.mem_map
added theorem Computation.mem_unique
added def Computation.pure
added theorem Computation.pure_def
added theorem Computation.ret_bind
added theorem Computation.ret_mem
added theorem Computation.ret_orElse
added def Computation.rmap
added def Computation.tail
added theorem Computation.tail_empty
added theorem Computation.tail_pure
added theorem Computation.tail_think
added theorem Computation.thinkN_mem
added theorem Computation.think_bind
added theorem Computation.think_mem
added def Computation