Lean4
/-- The set of program positions. We make extensive use of inductive types here to let us describe
"subroutines"; for example `clear p k q` is a program that clears stack `k`, then does `q` where
`q` is another label. In order to prevent this from resulting in an infinite number of distinct
accessible states, we are careful to be non-recursive (although loops are okay). See the section
documentation for a description of all the programs. -/
inductive Λ'
| move (p : Γ' → Bool) (k₁ k₂ : K') (q : Λ')
| clear (p : Γ' → Bool) (k : K') (q : Λ')
| copy (q : Λ')
| push (k : K') (s : Option Γ' → Option Γ') (q : Λ')
| read (f : Option Γ' → Λ')
| succ (q : Λ')
| pred (q₁ q₂ : Λ')
| ret (k : Cont')
