From 11e0f153deaa5236946fcbcec83eaab5ed94b432 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 29 Nov 2017 17:04:56 +0100
Subject: [PATCH] Add a test-case.

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

diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 51681a365..6c6cb5072 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -10,6 +10,16 @@ Section LiftingTests.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val → iProp Σ.
 
+  Definition simpl_test :
+    ⌜(10 = 4 + 6)%nat⌝ -∗
+    WP let: "x" := ref #1 in "x" <- !"x";; !"x" {{ v, ⌜v = #1⌝ }}.
+  Proof.
+    iIntros "?". wp_alloc l. repeat (wp_pure _) || wp_load || wp_store.
+    match goal with
+    | |- context [ (10 = 4 + 6)%nat ] => done
+    end.
+  Qed.
+
   Definition heap_e  : expr :=
     let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
 
-- 
GitLab