Commit e55b5ff8 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'stuck_fill' into 'master'

Add stuck_fill lemma.

See merge request iris/iris!276
parents 7dec6f7c 0df83ac0
......@@ -161,6 +161,10 @@ Section language.
to_val e = None irreducible e σ irreducible (K e) σ.
Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
Lemma stuck_fill `{!@LanguageCtx Λ K} e σ :
stuck e σ stuck (K e) σ.
Proof. intros [??]. split. by apply fill_not_val. by apply irreducible_fill. Qed.
Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) κ σ1 σ2 :
t1 t1' step (t1,σ1) κ (t2,σ2) t2', t2 t2' step (t1',σ1) κ (t2',σ2).
Proof.
......
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