Commit aea3b304 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix bug in step relation of language.

parent 9331a371
......@@ -34,13 +34,10 @@ Section language.
Inductive step (ρ1 ρ2 : cfg) : Prop :=
| step_atomic e1 σ1 e2 σ2 ef t1 t2 :
ρ1 = (t1 ++ e1 :: t2, σ1)
ρ1 = (t1 ++ e2 :: t2 ++ option_list ef, σ2)
ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2)
prim_step e1 σ1 e2 σ2 ef
step ρ1 ρ2.
Definition steps := rtc step.
Definition stepn := nsteps step.
Record is_ctx (K : E E) := IsCtx {
is_ctx_value e : to_val e = None to_val (K e) = None;
is_ctx_step_preserved e1 σ1 e2 σ2 ef :
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment