Theorems · Theorem · logic and foundations
Nat.Partrec.none
Nat.Partrec fun x => Part.none
- Defined in
- Mathlib.Computability.Partrec
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Part.Domproof · cited by 145
- Part.someproof · cited by 111
- Part.getproof · cited by 77
- Nat.pairproof · cited by 62
- PFun.liftproof · cited by 36
- Part.nonestatement · cited by 36
- Part.map_someproof · cited by 27
- Nat.Partrecstatement · cited by 19
- Nat.rfindproof · cited by 17
- Nat.Partrec.of_eqproof · cited by 14
- Part.eq_none_iffproof · cited by 6
- Nat.Partrec.of_primrecproof · cited by 6
Cited by2
Results whose statement or proof uses this declaration.
- Partrec.noneproof · cited by 3
- ComputablePred.halting_problemproof · cited by 1