Mathlib Map

Theorems · Theorem · logic and foundations

Nat.Partrec.Code.eval_part

Partrec₂ Nat.Partrec.Code.eval
Defined in
Mathlib.Computability.PartrecCode
Cited by
5 results in Mathlib
Foundations
Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Partrec.cond · cited by 3Partrec.condComputablePred.halting_problem_re · cited by 1ComputablePred.halting_pr…Nat.Partrec.Code.fixed_point · cited by 1Code.fixed_pointcomputable₂_ack · cited by 0computable₂_ackComputablePred.rice₂ · cited by 0ComputablePred.rice₂Nat.Partrec.Code · cited by 66Partrec.CodePrimrec.to_comp · cited by 40Primrec.to_compComputable.comp · cited by 31Computable.compNat.Partrec.Code.eval · cited by 25Code.evalComputable.snd · cited by 21Computable.sndPartrec₂ · cited by 20Partrec₂Partrec.of_eq · cited by 19Partrec.of_eqComputable.to₂ · cited by 17Computable.to₂Computable.fst · cited by 15Computable.fstNat.Partrec.Code.evaln · cited by 10Code.evalnNat.rfindOpt · cited by 9Nat.rfindOptComputable.pair · cited by 5Computable.pairNat.Partrec.Code.primrec_evaln · cited by 3Code.primrec_evalnNat.Partrec.Code.eval_eq_rfindOpt · cited by 2Code.eval_eq_rfindOptPartrec.rfindOpt · cited by 2Partrec.rfindOptCode.eval_partCITED BYCITES

Cites15

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

Cited by5

Results whose statement or proof uses this declaration.