mathlib documentation

data.seq.parallel

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

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

Equations
theorem computation.exists_of_mem_parallel {α : Type u} {S : wseq (computation α)} {a : α} (h : a computation.parallel S) :
(c : computation α) (H : c S), a c
def computation.parallel_rec {α : Type u} {S : wseq (computation α)} (C : α Sort v) (H : Π (s : computation α), s S Π (a : α), a s C a) {a : α} (h : a computation.parallel S) :
C a
Equations
theorem computation.parallel_promises {α : Type u} {S : wseq (computation α)} {a : α} (H : (s : computation α), s S s ~> a) :
theorem computation.mem_parallel {α : Type u} {S : wseq (computation α)} {a : α} (H : (s : computation α), s S s ~> a) {c : computation α} (cs : c S) (ac : a c) :
theorem computation.parallel_congr_lem {α : Type u} {S T : wseq (computation α)} {a : α} (H : wseq.lift_rel computation.equiv S T) :
( (s : computation α), s S s ~> a) (t : computation α), t T t ~> a