From df1cd3165dcba9ba22bd241939c65cd18965ec16 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 23 Sep 2020 10:16:50 +0200
Subject: [PATCH] Adressed nested binder encoding discrepancy

---
 papers/CPP21.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/papers/CPP21.md b/papers/CPP21.md
index c461674..dcc1f4c 100644
--- a/papers/CPP21.md
+++ b/papers/CPP21.md
@@ -13,6 +13,9 @@ contains an overview of the files in that directory.
   whereas that is written `∀ (X : lty k Σ). A` in Coq. This notation is used to
   for technical reasoning. The underlying definitions are the same between
   Coq and the paper.
+- The polymorphic session types are defined in an nested fashion, as a sequence
+  of quantifiers, followed by the actual type, for mechanisation purposes
+  using telescopes. The definitions are effectively identical to the paper.
 - The typing rule for branching (`ltyped_branch`) is written as a function
   instead of an n-ary rule with multiple premises.
 - The disjunction of the compute client invariant is encoded using a boolean
-- 
GitLab