Theorems · Theorem · logic and foundations

Turing.ToPartrec.cont_eval_fix

∀ {f : Turing.ToPartrec.Code} {k : Turing.ToPartrec.Cont} {v : List ℕ},
  f.Ok →
    StateTransition.eval Turing.ToPartrec.step (Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.fix f k) v) = do
      let v ← f.fix.eval v
      StateTransition.eval Turing.ToPartrec.step (Turing.ToPartrec.Cfg.ret k v)

Defined in

Mathlib.Computability.TuringMachine.Config

Cited by

2 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound