From 1a544253c6ae0c7eb6fa3a8081cba65085ddea2b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 7 Apr 2017 21:08:22 +0200
Subject: [PATCH] Fix a broken notation.
---
theories/lang/lang.v | 1 +
theories/lang/lib/lock.v | 7 ++-----
theories/lang/notation.v | 1 +
3 files changed, 4 insertions(+), 5 deletions(-)
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index c6bafa39..cadfc173 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -20,6 +20,7 @@ Inductive binder := BAnon | BNamed : string → binder.
Delimit Scope lrust_binder_scope with RustB.
Bind Scope lrust_binder_scope with binder.
+Notation "[ ]" := (@nil binder) : lrust_binder_scope.
Notation "a :: b" := (@cons binder a%RustB b%RustB)
(at level 60, right associativity) : lrust_binder_scope.
Notation "[ x1 ; x2 ; .. ; xn ]" :=
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index f82ad242..fa9f7b86 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -2,8 +2,7 @@ From iris.program_logic Require Import weakestpre.
From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl.
-From lrust.lang Require Import proofmode notation.
-From lrust.lang Require Export lang.
+From lrust.lang Require Import lang proofmode notation.
Set Default Proof Using "Type".
Definition newlock : val := λ: [], let: "l" := Alloc #1 in "l" <- #false ;; "l".
@@ -54,14 +53,12 @@ Section proof.
{ iNext. iExists false. by iFrame. }
eauto.
Qed.
-
Lemma newlock_spec (R : iProp Σ) :
{{{ ▷ R }}} newlock [] {{{ l γ, RET #l; is_lock γ l R }}}.
Proof.
- iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
+ iIntros (Φ) "HR HΦ". iApply wp_fupd.
wp_seq. wp_alloc l vl as "Hl" "H†". inv_vec vl=>x.
- (* FIXME: Something is wrong with the printing of the expression here *)
rewrite heap_mapsto_vec_singleton. (* FIXME shouldn't this also compute now, like bigops do? *)
wp_let. wp_write.
iMod (newlock_inplace with "[HR] Hl") as (γ) "?".
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 425839b1..8057d97f 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -12,6 +12,7 @@ Coercion Var : string >-> expr.
Coercion BNamed : string >-> binder.
Notation "<>" := BAnon : lrust_binder_scope.
+Notation "[ ]" := (@nil expr) : expr_scope.
Notation "[ x ]" := (@cons expr x%E (@nil expr)) : expr_scope.
Notation "[ x1 ; x2 ; .. ; xn ]" :=
(@cons expr x1%E (@cons expr x2%E
--
GitLab