Mathlib Map

Theorems · Inductive type · logic and foundations

Turing.ToPartrec.Code

Type

The type of codes for primitive recursive functions. Unlike Nat.Partrec.Code, this uses a set of operations on List ℕ. See Code.eval for a description of the behavior of the primitives.

Defined in
Mathlib.Computability.TuringMachine.Config
Cited by
83 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Turing.PartrecToTM2.tr · cited by 33PartrecToTM2.trTuring.ToPartrec.Code.eval · cited by 23Code.evalTuring.PartrecToTM2.trNormal · cited by 23PartrecToTM2.trNormalTuring.PartrecToTM2.codeSupp · cited by 16PartrecToTM2.codeSuppTuring.PartrecToTM2.codeSupp' · cited by 13PartrecToTM2.codeSupp'Turing.ToPartrec.stepNormal · cited by 13ToPartrec.stepNormalTuring.ToPartrec.Cont.brecOn.go · cited by 6brecOn.goTuring.ToPartrec.Cont.below · cited by 6Cont.belowTuring.ToPartrec.Code.brecOn.go · cited by 5brecOn.goTuring.ToPartrec.Cont.brecOn.eq · cited by 5brecOn.eqTuring.ToPartrec.Code.below · cited by 5Code.belowTuring.ToPartrec.Code.nil · cited by 5Code.nilTuring.ToPartrec.Code.brecOn.eq · cited by 4brecOn.eqTuring.ToPartrec.Code.comp_eval · cited by 4Code.comp_evalTuring.ToPartrec.Code.cons_eval · cited by 4Code.cons_evalToPartrec.CodeCITED BYCITES

Cites0

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

Nothing in Mathlib beyond the foundations.

Cited by149

Results whose statement or proof uses this declaration.