Operational

inductive Program (inst) : Type -> Type :=
| Ret {} : Π r,
    FreeM inst r
| Bind : Π {a r},
    (a -> FreeM inst r) -> (FreeM inst a) -> (FreeM inst r)
| Tag : Π {r}, inst r -> FreeM p r

abbreviation Prompt := Type -> Type -> Type

definition type_has_zero : has_zero Type₁ :=
    {| has_zero Type₁, zero := empty |}

definition type_has_one [instance] : has_one Type₁ :=
    {| has_one Type₁, one := unit |}

definition type_has_add [instance] : has_add Type :=
    {| has_add Type, add := sum |}

inductive StateP (S : Type₁) : Type₁ -> Type₁ -> Type₁ :=
| Get : StateP S S
| Set : StateP S (S -> 1)

abbreviation StateM S := FreeM (StateP S)

definition