Commit 67bef9f9 authored by Glen Mével's avatar Glen Mével

fix `head_stuck`

parent 1ab890fc
Pipeline #8381 failed with stage
in 0 seconds
...@@ -101,7 +101,7 @@ Section ectx_language. ...@@ -101,7 +101,7 @@ Section ectx_language.
Definition head_irreducible (e : expr Λ) (σ : state Λ) := Definition head_irreducible (e : expr Λ) (σ : state Λ) :=
e' σ' efs, ¬head_step e σ e' σ' efs. e' σ' efs, ¬head_step e σ e' σ' efs.
Definition head_stuck (e : expr Λ) (σ : state Λ) := Definition head_stuck (e : expr Λ) (σ : state Λ) :=
to_val e = None K e', e = fill K e' head_irreducible e' σ. to_val e = None head_irreducible e σ.
(* All non-value redexes are at the root. In other words, all sub-redexes are (* All non-value redexes are at the root. In other words, all sub-redexes are
values. *) values. *)
...@@ -168,9 +168,8 @@ Section ectx_language. ...@@ -168,9 +168,8 @@ Section ectx_language.
Lemma head_stuck_stuck e σ : Lemma head_stuck_stuck e σ :
head_stuck e σ sub_redexes_are_values e stuck e σ. head_stuck e σ sub_redexes_are_values e stuck e σ.
Proof. Proof.
move=>[] ? Hirr ?. split; first done. intros [] ?. split; first done.
apply prim_head_irreducible; last done. by apply prim_head_irreducible.
apply (Hirr empty_ectx). by rewrite fill_empty.
Qed. Qed.
Lemma ectx_language_atomic a e : Lemma ectx_language_atomic a e :
......
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