From b54a4dc95f0e569f4d9781916ab1a5690ee8969c Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Thu, 23 Apr 2020 16:17:16 +0200
Subject: [PATCH] Added pair typing example

---
 _CoqProject                     |  1 +
 theories/logrel/examples/pair.v | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 theories/logrel/examples/pair.v

diff --git a/_CoqProject b/_CoqProject
index f501a6e..033fbd5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -23,3 +23,4 @@ theories/logrel/session_types.v
 theories/logrel/types.v
 theories/logrel/subtyping.v
 theories/logrel/examples/double.v
+theories/logrel/examples/pair.v
diff --git a/theories/logrel/examples/pair.v b/theories/logrel/examples/pair.v
new file mode 100644
index 0000000..aea603b
--- /dev/null
+++ b/theories/logrel/examples/pair.v
@@ -0,0 +1,18 @@
+From iris.heap_lang Require Import notation proofmode.
+From actris.channel Require Import channel proto proofmode.
+From actris.logrel Require Export types.
+
+Definition prog : expr := λ: "c", (recv "c", recv "c").
+
+Section pair.
+  Context `{heapG Σ, chanG Σ}.
+
+  Lemma prog_typed :
+    ⊢ ∅ ⊨ prog : chan (<??> lty_int; <??> lty_int; END) ⊸ lty_int * lty_int.
+  Proof.
+    rewrite /prog.
+    iApply ltyped_lam. iApply ltyped_pair.
+    iApply ltyped_recv. iApply ltyped_recv.
+  Qed.
+
+End pair.
-- 
GitLab