Theorems · Definition · logic and foundations
Computation.destruct
{α : Type u} → Computation α → α ⊕ Computation αdestruct c is the destructor for Computation α as a coinductive type.
It returns inl a if c = pure a and inr c' if c = think c'.
- Defined in
- Mathlib.Data.Seq.Computation
- Cited by
- 37 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.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Computationstatement and proof · cited by 182
- Computation.tailproof · cited by 14
Cited by43
Results whose statement or proof uses this declaration.
- Computation.destruct_thinkstatement and proof · cited by 21
- Computation.corec_eqstatement · cited by 15
- Computation.eq_of_bisimproof · cited by 12
- Computation.recOnproof · cited by 11
- Stream'.WSeq.flattenproof · cited by 10
- Computation.destruct_eq_purestatement · cited by 10
- Computation.destruct_eq_thinkstatement · cited by 10
- Computation.ret_bindproof · cited by 7
- Computation.think_bindproof · cited by 7
- Stream'.WSeq.flatten_pureproof · cited by 6
- Computation.bind_pureproof · cited by 5
- Stream'.WSeq.destruct_flattenproof · cited by 4