diff --git a/heap_lang/notation.v b/heap_lang/notation.v index e95e8907e9e7782ba531346a5937d957477b0fd8..4325f3f4a76e51287a9cff454fa3697c8330c9e0 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 b86a28823808ec21864535716cf18fd795f17c05..28df58ed1b91cd01e259c26ef790a9b7a93f6954 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.