Theorems · Theorem · logic and foundations
Computation.parallel_empty
∀ {α : Type u} (S : Stream'.WSeq (Computation α)), S.head.Promises none → Computation.parallel S = Computation.empty α- Defined in
- Mathlib.Data.Seq.Parallel
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 41 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Computationstatement and proof · cited by 182
- Stream'.WSeqstatement and proof · cited by 149
- Computation.Terminatesproof · cited by 48
- Stream'.WSeq.get?proof · cited by 19
- Stream'.WSeq.headstatement and proof · cited by 17
- Computation.Promisesstatement and proof · cited by 13
- Computation.emptystatement · cited by 11
- Computation.parallelstatement and proof · cited by 8
- Stream'.WSeq.exists_get?_of_memproof · cited by 5
- Computation.exists_of_mem_parallelproof · cited by 3
- Stream'.WSeq.head_some_of_get?_someproof · cited by 1
- Computation.eq_empty_of_not_terminatesproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.