Theorems · Definition · logic and foundations
Partrec
{α : Type u_1} → {σ : Type u_2} → [Primcodable α] → [Primcodable σ] → (α →. σ) → PropPartially recursive partial functions α → σ between Primcodable types
- Defined in
- Mathlib.Computability.Partrec
- Cited by
- 48 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
- Assumes
- PrimcodablePrimcodable
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Primcodablestatement and proof · cited by 325
- PFunstatement and proof · cited by 207
- Encodable.encodeproof · cited by 118
- Encodable.decodeproof · cited by 77
- Part.bindproof · cited by 70
- Part.mapproof · cited by 65
- Part.ofOptionproof · cited by 33
- Nat.Partrecproof · cited by 19
Cited by51
Results whose statement or proof uses this declaration.
- Computableproof · cited by 80
- Partrec₂proof · cited by 20
- Partrec.of_eqstatement and proof · cited by 19
- Partrec.compstatement and proof · cited by 12
- Partrec.bindstatement and proof · cited by 10
- Partrec.to₂statement and proof · cited by 9
- Partrec.mapstatement and proof · cited by 8
- Partrec.nat_iffstatement · cited by 8
- Partrec₂.compstatement · cited by 8
- REPredproof · cited by 7
- Computable.ofOptionstatement · cited by 7
- Partrec.recursiveInstatement and proof · cited by 6