From 79bf7df88b3f698c06c2748ebbd787b317c6c6d0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Feb 2016 23:19:25 +0100
Subject: [PATCH] Use ;; for seq, ; conflicts with lists.
---
heap_lang/notation.v | 2 +-
heap_lang/tests.v | 9 ++-------
2 files changed, 3 insertions(+), 8 deletions(-)
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index e95e8907e..4325f3f4a 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -50,5 +50,5 @@ Notation "λ: x , e" := (LamV x e%L)
(at level 102, x at level 1, e at level 200) : lang_scope.
Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L)
(at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
-Notation "e1 ; e2" := (Lam "" e2%L e1%L)
+Notation "e1 ;; e2" := (Lam "" e2%L e1%L)
(at level 100, e2 at level 200) : lang_scope.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index b86a28823..28df58ed1 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -27,7 +27,7 @@ Module LiftingTests.
Implicit Types Q : val → iProp heap_lang Σ.
Definition e : expr :=
- let: "x" := ref '1 in "x" <- !"x" + '1; !"x".
+ let: "x" := ref '1 in "x" <- !"x" + '1;; !"x".
Goal ∀ σ E, ownP (Σ:=Σ) σ ⊑ wp E e (λ v, v = ('2)%L).
Proof.
move=> σ E. rewrite /e.
@@ -86,10 +86,6 @@ Module LiftingTests.
by rewrite -!later_intro -wp_value' // and_elim_r.
Qed.
- (* FIXME : For now apparent reason, I cannot prove this inline. *)
- Lemma Pred_sub_helper n : n - 1 = - (- n + 2 - 1).
- Proof. intros. omega. Qed.
-
Lemma Pred_spec n E Q : ▷ Q (LitV (n - 1)) ⊑ wp E (Pred 'n)%L Q.
Proof.
rewrite -wp_lam //=.
@@ -97,8 +93,7 @@ Module LiftingTests.
apply later_mono, wp_le=> Hn.
- rewrite -wp_if_true.
rewrite -(wp_bindi (UnOpCtx _)).
- (* FIXME use list notation. *)
- rewrite -(wp_bind ((AppLCtx _)::(AppRCtx FindPred)::nil)).
+ rewrite -(wp_bind [AppLCtx _; AppRCtx FindPred]).
rewrite -(wp_bindi (BinOpLCtx _ _)).
rewrite -wp_un_op //=.
rewrite -wp_bin_op //= -!later_intro.
--
GitLab