Commit 92085d3a authored by Dan Frumin's avatar Dan Frumin

Fix spacing

parent 66710e16
......@@ -66,8 +66,7 @@ Section proofs.
iApply "H".
Qed.
Lemma a_if_spec R Φ Ψ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
Lemma a_if_spec R Φ Ψ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
AsVal e1 ->
AsVal e2 ->
awp e R Ψ -
......@@ -102,8 +101,6 @@ Section proofs.
iIntros (? ->). iRight. iSplit; eauto. by awp_seq.
Qed.
Lemma a_seq_spec R Φ :
U (Φ #()) -
awp (a_seq #()) R Φ.
......@@ -148,8 +145,6 @@ Section proofs.
iModIntro. by awp_lam.
Qed.
Lemma a_load_spec R Φ Ψ e :
awp e R (λ v, l : loc, v = #l Ψ l) -
( l : loc, Ψ l - v, l U v (l U v - Φ v)) -
......
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