Commit 97f7dfb3 authored by Ralf Jung's avatar Ralf Jung

test awp_apply without

parent d4942fbf
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
aheap : atomic_heap Σ
Q : iProp Σ
l : loc
v : val
============================
"Hl" : l ↦ v
--------------------------------------∗
AACC << ∀ (v0 : val) (q : Qp), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
<< l ↦{q} v0, COMM Q -∗ Q >>
1 subgoal 1 subgoal
Σ : gFunctors Σ : gFunctors
......
From iris.heap_lang Require Export lifting notation. From iris.heap_lang Require Export lifting notation.
From iris.program_logic Require Export atomic. From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation atomic_heap.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Section tests.
Context `{!heapG Σ} {aheap: atomic_heap Σ}.
Import atomic_heap.notation.
(* FIXME: removing the `val` type annotation breaks printing. *)
Lemma test_awp_apply_without (Q : iProp Σ) (l : loc) v :
Q - l v - WP !#l {{ _, Q }}.
Proof.
iIntros "HQ Hl". awp_apply load_spec without "HQ". Show.
iAaccIntro with "Hl"; eauto with iFrame.
Qed.
End tests.
(* Test if AWP and the AU obtained from AWP print. *) (* Test if AWP and the AU obtained from AWP print. *)
Section printing. Section printing.
Context `{!heapG Σ}. Context `{!heapG Σ}.
......
...@@ -246,7 +246,7 @@ Lemma wp_frame_wand_l s E e Q Φ : ...@@ -246,7 +246,7 @@ Lemma wp_frame_wand_l s E e Q Φ :
Proof. Proof.
iIntros "[HQ HWP]". iApply (wp_wand with "HWP"). iIntros "[HQ HWP]". iApply (wp_wand with "HWP").
iIntros (v) "HΦ". by iApply "HΦ". iIntros (v) "HΦ". by iApply "HΦ".
Qed. Qed.
End wp. End wp.
......
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