Commit f23e484b authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Minor clean-up

parent 82c001dd
......@@ -4,28 +4,6 @@ From iris.algebra Require Import excl auth.
From iris.base_logic.lib Require Import auth.
Set Default Proof Using "Type".
(* Definition exclUR (A : Type) : ucmraT := *)
(* optionUR (exclR (leibnizC A)). *)
(* Definition to_auth_excl {A : Type} (a : A) : exclUR A := *)
(* Excl' (a: leibnizC A). *)
(* Section auth_excl. *)
(* Class auth_exclG (A : Type) (Σ :gFunctors) := *)
(* AuthExclG { *)
(* exclG_authG :> authG Σ (exclUR A); *)
(* }. *)
(* Definition auth_exclΣ (A : Type) : gFunctors := *)
(* #[GFunctor (authR (exclUR A))]. *)
(* Instance subG_auth_exclG {Σ} (A : Type) : *)
(* subG (auth_exclΣ) Σ → (auth_exclG) Σ. *)
(* Proof. solve_inG. Qed. *)
(* End auth_excl. *)
Definition exclUR (A : Type) : ucmraT :=
optionUR (exclR (leibnizC A)).
......@@ -46,7 +24,7 @@ Definition to_auth_excl {A : Type} (a : A) : exclUR A :=
Section auth_excl.
Context `{!auth_exclG A Σ} (N : namespace).
Context `{!auth_exclG A Σ}.
Lemma excl_eq γ x y :
own γ ( to_auth_excl y) - own γ ( to_auth_excl x) - x = y%I.
......@@ -63,7 +41,8 @@ Section auth_excl.
Qed.
Lemma excl_update γ x y z :
own γ ( to_auth_excl y) - own γ ( to_auth_excl x) - |==> own γ ( to_auth_excl z) own γ ( to_auth_excl z).
own γ ( to_auth_excl y) - own γ ( to_auth_excl x) ==
own γ ( to_auth_excl z) own γ ( to_auth_excl z).
Proof.
iIntros "Hauth Hfrag".
iDestruct (own_update_2 with "Hauth Hfrag") as "H".
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From stdpp Require Import gmap.
From iris.base_logic Require Import invariants.
Require Import FunctionalExtensionality.
Section typing.
(* Sides *)
Inductive side : Set :=
| Left
| Right.
(* Session Types *)
Inductive stype :=
| TEnd
| TSend (P : heap_lang.val Prop) (sτ : heap_lang.val stype)
| TRecv (P : heap_lang.val Prop) (sτ : heap_lang.val stype).
| TSend (P : val Prop) (sτ : val stype)
| TRecv (P : val Prop) (sτ : val stype).
Fixpoint dual_stype (sτ :stype) :=
match sτ with
......
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