From 9456e121b2df1b355fd90b6a698b42a890f47d0c Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 6 May 2020 20:51:26 +0200
Subject: [PATCH] Updated header for channel.v

---
 theories/channel/channel.v | 5 ++++-
 theories/channel/proto.v   | 2 +-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 2c82031..9ed9b22 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -17,7 +17,10 @@ In this file we define the three message-passing connectives:
   polarity of the endpoints.
 - [send] takes an endpoint and adds an element to the first buffer.
 - [recv] performs a busy loop until there is something in the second buffer,
-  which it pops and returns, locking during each peek.*)
+  which it pops and returns, locking during each peek.
+
+It is additionaly shown that the channel ownership [c ↣ prot] is closed under
+the subprotocol relation [⊑] *)
 From iris.heap_lang Require Export lifting notation.
 From iris.heap_lang Require Import proofmode.
 From iris.heap_lang.lib Require Import spin_lock.
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 012eb27..f483fa0 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -27,7 +27,7 @@ Futhermore, we define the following operations:
 - [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa
 - [iProto_app], which appends two protocols as described in proto_model.v
 
-In addition we define the [iProto_le] subprotocol relation, which generalises
+In addition we define the subprotocol relation [iProto_le] [⊑], which generalises
 the following inductive definition for asynchronous subtyping on session types:
 
                  p1 <: p2           p1 <: p2          p1 <: !B.p3    ?A.p3 <: p2
-- 
GitLab