Right now instructions are typed against a stack, while programs are not:
Inductive has_prog_type : program -> instr_type -> Prop :=
with has_instr_type : instr -> stack -> instr_type -> Prop :=
My opinion is that they should be typed the same way, and I lean towards both without a stack, but I think this needs more discussion.
Right now instructions are typed against a stack, while programs are not:
Inductive has_prog_type : program -> instr_type -> Prop :=with has_instr_type : instr -> stack -> instr_type -> Prop :=My opinion is that they should be typed the same way, and I lean towards both without a stack, but I think this needs more discussion.