Mathlib Map

Theorems · Inductive type · logic and foundations

Nat.Partrec

(ℕ →. ℕ) → Prop

Nat.Partrec f means that the partial function f : ℕ →. ℕ is partially recursive.

Defined in
Mathlib.Computability.Partrec
Cited by
19 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Partrec · cited by 48PartrecNat.Partrec.of_eq · cited by 14Partrec.of_eqPartrec.nat_iff · cited by 8Partrec.nat_iffNat.Partrec.of_primrec · cited by 6Partrec.of_primrecNat.Partrec.Code.exists_code · cited by 5Code.exists_codeNat.Partrec.ppred · cited by 4Partrec.ppredNat.Partrec.recursiveIn · cited by 2Partrec.recursiveInNat.Partrec.some · cited by 2Partrec.someComputablePred.rice · cited by 2ComputablePred.riceNat.Partrec'.of_part · cited by 2Partrec'.of_partNat.Partrec.none · cited by 2Partrec.noneNat.Partrec.prec' · cited by 1Partrec.prec'Nat.Partrec.rfind' · cited by 1Partrec.rfind'Partrec.bind_decode₂_iff · cited by 1Partrec.bind_decode₂_iffPartrec.merge' · cited by 1Partrec.merge'PFun · cited by 207PFunNat.PartrecCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • PFunstatement · cited by 207

Cited by24

Results whose statement or proof uses this declaration.