Theorems · Theorem · logic and foundations

Turing.ToPartrec.Cont.eval.eq_def

∀ (x : Turing.ToPartrec.Cont),
  x.eval =
    match x with
    | Turing.ToPartrec.Cont.halt => pure
    | Turing.ToPartrec.Cont.cons₁ fs as k => fun v => do
      let ns ← fs.eval as
      k.eval (v.headI :: ns)
    | Turing.ToPartrec.Cont.cons₂ ns k => fun v => k.eval (ns.headI :: v)
    | Turing.ToPartrec.Cont.comp f k => fun v => f.eval v >>= k.eval
    | Turing.ToPartrec.Cont.fix f k => fun v => if v.headI = 0 then k.eval v.tail else f.fix.eval v.tail >>= k.eval

Defined in

Mathlib.Computability.TuringMachine.Config

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses no axioms