From 5da00edc9f0f32ba373fe1dc46e4309454db174f Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 6 May 2020 23:24:31 +0200
Subject: [PATCH] Nits

---
 theories/logrel/model.v         | 8 ++++----
 theories/logrel/session_types.v | 4 ++--
 theories/logrel/term_types.v    | 8 +++-----
 3 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/theories/logrel/model.v b/theories/logrel/model.v
index d38d587..3d55815 100644
--- a/theories/logrel/model.v
+++ b/theories/logrel/model.v
@@ -1,9 +1,9 @@
 (** This file contains the definition of what semantic term types and semantic
-session types are. A semantic term type is a unary (Iris) predicate on values,
-as is customary in a logical relation for type soundness. A semantic session
-type is essentially an Actris protocol.
+session types are. A semantic term type is a unary (Iris) predicate on values
+[val → iProp], as is customary in a logical relation for type soundness.
+A semantic session type is an Actris protocol [iProto].
 
-There is a single variant [lty Σ k], which contains either a term type or a
+There is a single kinded variant [lty Σ k], which contains either a term type or a
 session type, depending on the kind [k]. The reason for having a single type
 containing both term types and session types is that it allows for uniform
 definitions of polymorphic binders for term types and session types, instead of
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index d4dff05..e772044 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -1,7 +1,7 @@
-(** This file defines the semantic interpretations of sesssion types as Actris
+(** This file defines the semantic interpretations of session types as Actris
 protocols. It includes session types for sending and receiving with session
 polymorphism, as well as n-ary choice. Recursive protocols are defined in
-[model.v]. *)
+the model.v file. *)
 From iris.algebra Require Export gmap.
 From actris.logrel Require Export model kind_tele.
 From actris.channel Require Export channel.
diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index baf91a6..b29cec1 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -4,21 +4,19 @@ term type formers of the type system. The semantic interpretation of a type
 when a value belongs to a certain type.
 
 The following types are defined:
-
 - [unit], [bool], [int]: basic types for unit, boolean and integer values,
   respectively.
 - [any]: inhabited by all values.
 - [A ⊸ B]: the type of affine functions from [A] to [B]. Affine functions can
   only be invoked once, since they might have captured affine resources.
 - [A → B]: the type of non-affine (copyable) functions from [A] to [B]. These
-  can be invoked any number of times. This is simply syntactic sugar for [copy
-  (A ⊸ B)].
+  can be invoked any number of times. This is simply syntactic sugar for
+  [copy (A ⊸ B)].
 - [A * B], [A + B], [∀ X, A], [∃ X, A]: products, sums, universal types,
   existential types.
 - [copy A]: inhabited by those values in the type [A] which are copyable. In the
   case of functions, for instance, functions (closures) which capture affine
-  resources are not copyable, whereas functions that do not capture resources
-  are.
+  resources are not copyable, whereas functions that do not capture resources are.
 - [copy- A]: acts as a kind of "inverse" to [copy A]. More precisely, we have
   that [copy- (copy A) <:> A]. This type is used to indicate the results of
   operations that might consume a resource, but do not always do so, depending
-- 
GitLab