Theorems · Definition · logic and foundations

Computation.parallelRec

{α : Type u} →
  {S : Stream'.WSeq (Computation α)} →
    (C : α → Sort v) →
      ((s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a) → {a : α} → a ∈ Computation.parallel S → C a

Induction principle for parallel computations. The reason this isn't trivial from exists_of_mem_parallel is because it eliminates to Sort.

Defined in

Mathlib.Data.Seq.Parallel

Cited by

0 results in Mathlib

Foundations

Depth 41 from the axioms · uses propext, Classical.choice, Quot.sound