Mathlib Map

Theorems · Inductive type · logic and foundations

Turing.ToPartrec.Cont

Type

The type of continuations, built up during evaluation of a Code expression.

Defined in
Mathlib.Computability.TuringMachine.Config
Cited by
33 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.ToPartrec.stepNormal · cited by 13ToPartrec.stepNormalTuring.ToPartrec.step · cited by 7ToPartrec.stepTuring.ToPartrec.Cont.brecOn.go · cited by 6brecOn.goTuring.ToPartrec.Cont.below · cited by 6Cont.belowTuring.PartrecToTM2.TrCfg · cited by 5PartrecToTM2.TrCfgTuring.ToPartrec.Cont.brecOn.eq · cited by 5brecOn.eqTuring.ToPartrec.stepRet · cited by 5ToPartrec.stepRetTuring.ToPartrec.Cont.then · cited by 5Cont.thenTuring.PartrecToTM2.contStack · cited by 3PartrecToTM2.contStackTuring.PartrecToTM2.trCont · cited by 3PartrecToTM2.trContTuring.ToPartrec.Cfg.then · cited by 3Cfg.thenTuring.ToPartrec.Code.Ok · cited by 3Code.OkTuring.ToPartrec.Cont.eval · cited by 3Cont.evalTuring.PartrecToTM2.trContStack · cited by 2PartrecToTM2.trContStackTuring.PartrecToTM2.trNormal_respects · cited by 2PartrecToTM2.trNormal_res…ToPartrec.ContCITED 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 by72

Results whose statement or proof uses this declaration.