Theorems · Theorem · logic and foundations
Turing.ToPartrec.Code.comp_eval
∀ (f g : Turing.ToPartrec.Code), (f.comp g).eval = fun v => g.eval v >>= f.eval
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Partstatement · cited by 325
- PFunstatement · cited by 207
- Turing.ToPartrec.Codestatement and proof · cited by 83
- Part.bindproof · cited by 70
- Turing.ToPartrec.Code.evalstatement and proof · cited by 23
Cited by4
Results whose statement or proof uses this declaration.
- Turing.ToPartrec.Code.nil_evalproof · cited by 4
- Turing.ToPartrec.Code.id_evalproof · cited by 2
- Turing.ToPartrec.Code.exists_code.compproof · cited by 1
- Turing.ToPartrec.Code.exists_codeproof · cited by 0