Theorems · Definition · logic and foundations
Computation.Promises
{α : Type u} → Computation α → α → PropPromises s a, or s ~> a, asserts that although the computation s
may not terminate, if it does, then the result is a.
- Defined in
- Mathlib.Data.Seq.Computation
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Computationstatement and proof · cited by 182
Cited by13
Results whose statement or proof uses this declaration.
- Computation.mem_of_promisesstatement and proof · cited by 2
- Computation.parallel_congr_lemstatement and proof · cited by 2
- Computation.parallel_promisesstatement and proof · cited by 2
- Computation.mem_parallelstatement and proof · cited by 1
- Computation.parallel_congr_leftstatement and proof · cited by 1
- Computation.promises_congrstatement · cited by 1
- Computation.mem_promisesstatement · cited by 0
- Computation.get_eq_of_promisesstatement · cited by 0
- Computation.get_promisesstatement · cited by 0
- Computation.parallel_congr_rightstatement and proof · cited by 0
- Computation.parallel_emptystatement and proof · cited by 0
- Computation.bind_promisesstatement and proof · cited by 0