Theorems · Theorem · logic and foundations
Computation.corec_eq
∀ {α : Type u} {β : Type v} (f : β → α ⊕ β) (b : β),
(Computation.corec f b).destruct = Computation.rmap (Computation.corec f) (f b)- Defined in
- Mathlib.Data.Seq.Computation
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Stream'proof · cited by 205
- Computationstatement and proof · cited by 182
- Stream'.tailproof · cited by 68
- Computation.destructstatement · cited by 37
- Computation.corecstatement · cited by 18
- Computation.tailproof · cited by 14
- Stream'.tail_consproof · cited by 11
- Computation.rmapstatement · cited by 6
- Stream'.corec'proof · cited by 3
- Stream'.corec'_eqproof · cited by 2
- Computation.Corec.fproof · cited by 1
Cited by15
Results whose statement or proof uses this declaration.
- Stream'.WSeq.destruct_thinkproof · cited by 12
- Stream'.WSeq.destruct_consproof · cited by 11
- Computation.think_bindproof · cited by 7
- Computation.ret_bindproof · cited by 7
- Computation.exists_of_mem_parallelproof · cited by 3
- Stream'.WSeq.destruct_ofSeqproof · cited by 2
- Stream'.WSeq.toList'_consproof · cited by 2
- Computation.orElse_thinkproof · cited by 2
- Computation.terminates_parallelproof · cited by 1
- Computation.ret_orElseproof · cited by 1
- Stream'.WSeq.toList'_thinkproof · cited by 1
- Computation.orElse_pureproof · cited by 1