From 8e4f1524caab26319a95a4422431435bce3e1360 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 20 Sep 2017 12:30:26 +0200
Subject: [PATCH] Add a `repeat (wp_pure _)` example.

---
 theories/tests/heap_lang.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 5cfbe477a..8db1ef4e7 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -31,6 +31,17 @@ Section LiftingTests.
     wp_load. wp_op. wp_store. wp_load. done.
   Qed.
 
+  Definition heap_e3 : expr :=
+    let: "x" := #true in
+    let: "f" := λ: "z", "z" + #1 in
+    if: "x" then "f" #0 else "f" #1.
+
+  Lemma heap_e3_spec E : WP heap_e3 @ E {{ v, ⌜v = #1⌝ }}%I.
+  Proof.
+    iIntros "". rewrite /heap_e3.
+    by repeat (wp_pure _).
+  Qed.
+
   Definition FindPred : val :=
     rec: "pred" "x" "y" :=
       let: "yp" := "y" + #1 in
-- 
GitLab