diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v index 87ed6c41f1e3ff5acbe6467b6acfb0cc69ea0eed..0d6d2c8d9ea3afbab492c3f0c1075947635b5a30 100644 --- a/theories/tests/heap_lang.v +++ b/theories/tests/heap_lang.v @@ -104,6 +104,11 @@ Section LiftingTests. Lemma Pred_user E : WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌠}]%I. Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed. + + Lemma wp_apply_evar e : + (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}. + Proof. iIntros "H". wp_apply "H". done. Qed. + End LiftingTests. Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).