From 6045937eba7b241a6491a8f55ad7483a24eacb65 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 1 May 2020 19:33:36 +0200
Subject: [PATCH] Added notation for telescope message types
---
theories/logrel/session_types.v | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 14f4dfa..eecd13a 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -50,6 +50,9 @@ 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 "<!!.. 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.
@@ -57,6 +60,9 @@ 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 "<??.. 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.
--
GitLab