# mathlib3documentation

data.seq.parallel

Equations
Equations
def computation.parallel {α : Type u} (S : stream.wseq (computation α)) :

Parallel computation of an infinite stream of computations, taking the first result

Equations
theorem computation.terminates_parallel.aux {α : Type u} {l : list (computation α)} {S : stream.wseq (computation α)} {c : computation α} :
c l
theorem computation.terminates_parallel {α : Type u} {S : stream.wseq (computation α)} {c : computation α} (h : c S) [T : c.terminates] :
theorem computation.exists_of_mem_parallel {α : Type u} {S : stream.wseq (computation α)} {a : α} (h : a ) :
(c : (H : c S), a c
theorem computation.map_parallel {α : Type u} {β : Type v} (f : α β) (S : stream.wseq (computation α)) :
def computation.parallel_rec {α : Type u} {S : stream.wseq (computation α)} (C : α Sort v) (H : Π (s : , s S Π (a : α), a s C a) {a : α} (h : a ) :
C a
Equations
theorem computation.parallel_promises {α : Type u} {S : stream.wseq (computation α)} {a : α} (H : (s : , s S s ~> a) :
theorem computation.mem_parallel {α : Type u} {S : stream.wseq (computation α)} {a : α} (H : (s : , s S s ~> a) {c : computation α} (cs : c S) (ac : a c) :
theorem computation.parallel_congr_lem {α : Type u} {S T : stream.wseq (computation α)} {a : α}  :
( (s : , s S s ~> a) (t : , t T t ~> a
theorem computation.parallel_congr_left {α : Type u} {S T : stream.wseq (computation α)} {a : α} (h1 : (s : , s S s ~> a)  :
theorem computation.parallel_congr_right {α : Type u} {S T : stream.wseq (computation α)} {a : α} (h2 : (t : , t T t ~> a)  :