From 6da6e6b1b97d63cc5ed165921ddf398b51c058ef Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Apr 2016 12:40:56 +0200
Subject: [PATCH] Make levels of viewshifts consistent with implication/wand.

---
 program_logic/pviewshifts.v |  6 +++---
 program_logic/viewshifts.v  | 29 ++++++++++++++++++++++-------
 2 files changed, 25 insertions(+), 10 deletions(-)

diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 51c23f476..cd2ee4887 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -33,13 +33,13 @@ Arguments pvs {_ _} _ _ _%I.
 Instance: Params (@pvs) 4.
 
 Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
-  (at level 199, E1, E2 at level 50, Q at level 200,
+  (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 , E2 }=>  Q") : uPred_scope.
 Notation "|={ E }=> Q" := (pvs E E Q%I)
-  (at level 199, E at level 50, Q at level 200,
+  (at level 99, E at level 50, Q at level 200,
    format "|={ E }=>  Q") : uPred_scope.
 Notation "|==> Q" := (pvs ⊤ ⊤ Q%I)
-  (at level 199, Q at level 200, format "|==>  Q") : uPred_scope.
+  (at level 99, Q at level 200, format "|==>  Q") : uPred_scope.
 
 Section pvs.
 Context {Λ : language} {Σ : iFunctor}.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index eb1c91543..5bf652bac 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -8,15 +8,30 @@ Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
 Arguments vs {_ _} _ _ _%I _%I.
 Instance: Params (@vs) 4.
 Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I)
-  (at level 199, E1,E2 at level 50,
+  (at level 99, E1,E2 at level 50, Q at level 200,
    format "P  ={ E1 , E2 }=>  Q") : uPred_scope.
-Notation "P ={ E1 , E2 }=> Q" := (True ⊢ vs E1 E2 P%I Q%I)
-  (at level 199, E1, E2 at level 50,
+Notation "P ={ E1 , E2 }=> Q" := (True ⊢ (P ={E1,E2}=> Q)%I)
+  (at level 99, E1, E2 at level 50, Q at level 200,
    format "P  ={ E1 , E2 }=>  Q") : C_scope.
-Notation "P ={ E }=> Q" := (vs E E P%I Q%I)
-  (at level 199, E at level 50, format "P  ={ E }=>  Q") : uPred_scope.
-Notation "P ={ E }=> Q" := (True ⊢ vs E E P%I Q%I)
-  (at level 199, E at level 50, format "P  ={ E }=>  Q") : C_scope.
+Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=>  Q") : uPred_scope.
+Notation "P ={ E }=> Q" := (True ⊢ (P ={E}=> Q)%I)
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=>  Q") : C_scope.
+
+Notation "P <={ E1 , E2 }=> Q" := ((P ={E1,E2}=> Q) ∧ (Q ={E2,E1}=> P))%I
+  (at level 99, E1,E2 at level 50, Q at level 200,
+   format "P  <={ E1 , E2 }=>  Q") : uPred_scope.
+Notation "P <={ E1 , E2 }=> Q" := (True ⊢ (P <={E1,E2}=> Q)%I)
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "P  <={ E1 , E2 }=>  Q") : C_scope.
+Notation "P <={ E }=> Q" := (P <={E,E}=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P  <={ E }=>  Q") : uPred_scope.
+Notation "P <={ E }=> Q" := (True ⊢ (P <={E}=> Q)%I)
+  (at level 99, E at level 50, Q at level 200,
+   format "P  <={ E }=>  Q") : C_scope.
 
 Section vs.
 Context {Λ : language} {Σ : iFunctor}.
-- 
GitLab