From 40dfc35aad55f84168010765a9375e6b03a19177 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 25 May 2016 16:49:40 +0200
Subject: [PATCH] add missing file: lviewshifts

---
 _CoqProject                 |  1 +
 program_logic/lviewshifts.v | 23 +++++++++++++++++++++++
 2 files changed, 24 insertions(+)
 create mode 100644 program_logic/lviewshifts.v

diff --git a/_CoqProject b/_CoqProject
index 46417a253..b5191d5d9 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -68,6 +68,7 @@ program_logic/ownership.v
 program_logic/weakestpre.v
 program_logic/weakestpre_fix.v
 program_logic/pviewshifts.v
+program_logic/lviewshifts.v
 program_logic/resources.v
 program_logic/hoare.v
 program_logic/language.v
diff --git a/program_logic/lviewshifts.v b/program_logic/lviewshifts.v
new file mode 100644
index 000000000..694d15330
--- /dev/null
+++ b/program_logic/lviewshifts.v
@@ -0,0 +1,23 @@
+From iris.program_logic Require Export pviewshifts.
+Import uPred.
+
+(* Some notation for linear view shifts. *)
+
+Definition lvs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
+  (P -★ |={E1,E2}=> Q)%I.
+Arguments lvs {_ _} _ _ _%I _%I.
+Instance: Params (@lvs) 4.
+Notation "P ={ E1 , E2 }=★ Q" := (lvs E1 E2 P%I Q%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.
+
+(* TODO: Also prove some lemmas. *)
-- 
GitLab