Theorems · Inductive type · logic and foundations

Turing.TM2to1.StAct

(K : Type u_1) → (K → Type u_2) → Type u_4 → K → Type (max u_2 u_4)

A stack action is a command that interacts with the top of a stack. Our default position is at the bottom of all the stacks, so we have to hold on to this action while going to the end to modify the stack.

Defined in

Mathlib.Computability.TuringMachine.StackTuringMachine

Cited by

21 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms