mathlib documentation

data.seq.parallel

def computation.parallel.aux2 {α : Type u} :

Equations

Equations
def computation.parallel {α : Type u} :

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

Equations
theorem computation.terminates_parallel {α : Type u} {S : wseq (computation α)} {c : computation α} (h : c S) [T : c.terminates] :

theorem computation.exists_of_mem_parallel {α : Type u} {S : wseq (computation α)} {a : α} :
a computation.parallel S(∃ (c : computation α) (H : c S), a c)

theorem computation.map_parallel {α : Type u} {β : Type v} (f : α → β) (S : wseq (computation α)) :

def computation.parallel_rec {α : Type u} {S : wseq (computation α)} (C : α → Sort v) (H : Π (s : computation α), s SΠ (a : α), a sC a) {a : α} :

Equations
theorem computation.parallel_promises {α : Type u} {S : wseq (computation α)} {a : α} :
(∀ (s : computation α), s Ss ~> a)computation.parallel S ~> a

theorem computation.mem_parallel {α : Type u} {S : wseq (computation α)} {a : α} (H : ∀ (s : computation α), s Ss ~> a) {c : computation α} :
c Sa ca computation.parallel S

theorem computation.parallel_congr_lem {α : Type u} {S T : wseq (computation α)} {a : α} :
wseq.lift_rel computation.equiv S T((∀ (s : computation α), s Ss ~> a) ∀ (t : computation α), t Tt ~> a)

theorem computation.parallel_congr_left {α : Type u} {S T : wseq (computation α)} {a : α} :

theorem computation.parallel_congr_right {α : Type u} {S T : wseq (computation α)} {a : α} :