From 623b6232fed5fa511a23c1ee7fb24eb0bc6426a5 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 1 May 2020 19:44:28 +0200
Subject: [PATCH] Notation nits and fixed subtyping oversight

---
 theories/logrel/session_types.v   | 17 +++++++++--------
 theories/logrel/subtyping_rules.v |  8 ++++----
 2 files changed, 13 insertions(+), 12 deletions(-)

diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 38b610c..f0fae26 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -39,16 +39,17 @@ Notation "∃ x .. y , m" :=
 Notation "'END'" := lty_end : lty_scope.
 Notation "<!!> M" :=
   (lty_message Send M) (at level 200, M at level 200) : lty_scope.
-Notation "<!! x1 .. xn > M" :=
-  (lty_message Send (∃ x1, .. (∃ xn, M) ..))
-    (at level 200, x1 closed binder, xn closed binder, M at level 200,
-     format "<!!  x1  ..  xn >  M") : lty_scope.
+Notation "<!! X .. Y > M" :=
+  (<!!> ∃ X, .. (∃ Y, M) ..)%lty
+    (at level 200, X closed binder, Y closed binder, M at level 200,
+     format "<!!  X  ..  Y >  M") : lty_scope.
+
 Notation "<??> M" :=
   (lty_message Recv M) (at level 200, M at level 200) : lty_scope.
-Notation "<?? x1 .. xn > M" :=
-  (lty_message Recv (∃ x1, .. (∃ xn, M) ..))
-    (at level 200, x1 closed binder, xn closed binder, M at level 200,
-     format "<??  x1  ..  xn >  M") : lty_scope.
+Notation "<?? X .. Y > M" :=
+  (<??> ∃ X, .. (∃ Y, M) ..)%lty
+    (at level 200, X closed binder, Y closed binder, M at level 200,
+     format "<??  X  ..  Y >  M") : lty_scope.
 Notation lty_select := (lty_choice Send).
 Notation lty_branch := (lty_choice Recv).
 Infix "<++>" := lty_app (at level 60) : lty_scope.
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index c1a93a6..2ca2ea5 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -260,12 +260,12 @@ Section subtyping_rules.
   Proof. iIntros "#Hle !>". iApply (iProto_le_exist_elim_r_inhabited _ M). auto. Qed.
 
   Lemma lty_le_exist_intro_l k (M : lty Σ k → lmsg Σ) (A : lty Σ k) :
-    ⊢ (<! X> M X) ⊑ (<!> M A).
-  Proof. by iApply (iProto_le_exist_intro_l). Qed.
+    ⊢ (<!! X> M X) <: (<!!> M A).
+  Proof. iIntros "!>". iApply (iProto_le_exist_intro_l). Qed.
 
   Lemma lty_le_exist_intro_r k (M : lty Σ k → lmsg Σ) (A : lty Σ k) :
-    ⊢ (<?> M A) ⊑ (<? X> M X).
-  Proof. by iApply (iProto_le_exist_intro_r). Qed.
+    ⊢ (<??> M A) <: (<?? X> M X).
+  Proof. iIntros "!>". iApply (iProto_le_exist_intro_r). Qed.
 
   Lemma lty_le_swap_recv_send A1 A2 S :
     ⊢ (<??> TY A1; <!!> TY A2; S) <: (<!!> TY A2; <??> TY A1; S).
-- 
GitLab