Commit b54a4dc9 authored by Jonas Kastberg's avatar Jonas Kastberg

Added pair typing example

parent fb39403a
......@@ -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
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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment