Commit 2f6b8a24 authored by Ralf Jung's avatar Ralf Jung

shorten heap_lang/adequacy proof

parent 19c45f91
Pipeline #2814 passed with stage
in 9 minutes and 23 seconds
......@@ -20,9 +20,8 @@ Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
adequate e σ φ.
Proof.
intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
iVs (auth_alloc to_heap ownP heapN _ σ with "[Hσ]") as (γ) "[Hh _]".
iVs (auth_alloc to_heap _ heapN _ σ with "[Hσ]") as (γ) "[Hh _]";[|by iNext|].
{ exact: to_heap_valid. }
{ by iNext. }
set (Hheap := HeapG _ _ _ γ).
iApply (Hwp _). by rewrite /heap_ctx.
Qed.
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