From 5c2891cea3e3b2dea024ed137e6718a7060070ed Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Thu, 16 Apr 2020 11:39:51 +0200
Subject: [PATCH] Changed <++++> to an overload of <++>
---
theories/logrel/session_types.v | 2 +-
theories/logrel/subtyping.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index dc70d5a..372f36c 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -95,4 +95,4 @@ Notation "<!!> A ; P" :=
(lsty_send A P) (at level 20, A, P at level 200) : lsty_scope.
Notation "<??> A ; P" :=
(lsty_recv A P) (at level 20, A, P at level 200) : lsty_scope.
-Infix "<++++>" := lsty_app (at level 60) : lsty_scope.
+Infix "<++>" := lsty_app (at level 60) : lsty_scope.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 443e38e..9073812 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -285,7 +285,7 @@ Section subtype.
Lemma lsty_app_le P11 P12 P21 P22 :
(P11 <p: P21) -∗ (P12 <p: P22) -∗
- (P11 <++++> P12) <p: (P21 <++++> P22).
+ (P11 <++> P12) <p: (P21 <++> P22).
Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
Lemma lsty_dual_le P1 P2 : P2 <p: P1 -∗ lsty_dual P1 <p: lsty_dual P2.
--
GitLab