Theorems · Theorem · logic and foundations
Nat.Partrec.of_primrec
∀ {f : ℕ → ℕ}, Nat.Primrec f → Nat.Partrec ↑f- Defined in
- Mathlib.Computability.Partrec
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 27 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.
- Partproof · cited by 325
- Part.someproof · cited by 111
- Part.bindproof · cited by 70
- Nat.unpairproof · cited by 67
- Nat.pairproof · cited by 62
- Part.bind_someproof · cited by 49
- PFun.liftstatement and proof · cited by 36
- Part.map_someproof · cited by 27
- Nat.Primrecstatement and proof · cited by 25
- Nat.Partrecstatement and proof · cited by 19
- Nat.Partrec.of_eq_totproof · cited by 1
Cited by6
Results whose statement or proof uses this declaration.
- Primrec.to_compproof · cited by 40
- Nat.Partrec.ppredproof · cited by 4
- Nat.Partrec.someproof · cited by 2
- Nat.Partrec.noneproof · cited by 2
- Computable.bind_decode_iffproof · cited by 1
- Nat.Primrec.recursiveInproof · cited by 0