diff --git a/tests/heap_lang.v b/tests/heap_lang.v index 90ad0e2c2b9bf79bc26a2f8e55afe799da684dfb..efed8387ea57a950617af6781fabef9ea8e46f84 100644 --- a/tests/heap_lang.v +++ b/tests/heap_lang.v @@ -218,6 +218,18 @@ Section tests. iIntros "[$ _]". (* splits the fraction, not the app *) Qed. + + Lemma test_wp_free l v : + {{{ l ↦ v }}} Free #l {{{ RET #(); True }}}. + Proof. + iIntros (Φ) "Hl HΦ". wp_free. iApply "HΦ". done. + Qed. + + Lemma test_twp_free l v : + [[{ l ↦ v }]] Free #l [[{ RET #(); True }]]. + Proof. + iIntros (Φ) "Hl HΦ". wp_free. iApply "HΦ". done. + Qed. End tests. Section inv_mapsto_tests.