Theorems · Definition · logic and foundations
Computation.empty
(α : Type u_1) → Computation α
empty α is the computation that never returns, an infinite sequence of
thinks.
- Defined in
- Mathlib.Data.Seq.Computation
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Computationstatement · cited by 182
- Stream'.constproof · cited by 11
Cited by11
Results whose statement or proof uses this declaration.
- Computation.think_emptystatement · cited by 2
- Computation.notMem_emptystatement and proof · cited by 2
- Computation.destruct_emptystatement · cited by 1
- Computation.eq_empty_of_not_terminatesstatement · cited by 1
- Computation.not_terminates_emptystatement and proof · cited by 0
- Computation.parallel_emptystatement · cited by 0
- Computation.tail_emptystatement · cited by 0
- Computation.orElse_emptystatement and proof · cited by 0
- Computation.head_emptystatement · cited by 0
- Computation.empty_orElsestatement and proof · cited by 0
- Computation.empty_promisesstatement and proof · cited by 0