Theorems · Definition · logic and foundations
Computation.pure
{α : Type u} → α → Computation αpure a is the computation that immediately terminates with result a.
- Defined in
- Mathlib.Data.Seq.Computation
- Cited by
- 61 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 by67
Results whose statement or proof uses this declaration.
- Computation.ret_memstatement · cited by 13
- Stream'.WSeq.destruct_nilstatement · cited by 12
- Computation.eq_of_bisimproof · cited by 12
- Computation.recOnstatement and proof · cited by 11
- Stream'.WSeq.destruct_consstatement · cited by 11
- Computation.destruct_eq_purestatement and proof · cited by 10
- Computation.ret_bindstatement and proof · cited by 7
- Stream'.WSeq.flatten_purestatement and proof · cited by 6
- Computation.exists_of_mem_mapproof · cited by 6
- Stream'.WSeq.exists_get?_of_memproof · cited by 5
- Computation.bind_purestatement and proof · cited by 5
- Computation.memRecOnstatement and proof · cited by 5