Commit 708450ba authored by Jonas Kastberg's avatar Jonas Kastberg

Bumped move of Atomic to Iris

parent 7f46144d
......@@ -5,7 +5,6 @@ theories/utils/llist.v
theories/utils/compare.v
theories/utils/contribution.v
theories/utils/group.v
theories/utils/misc.v
theories/channel/channel.v
theories/channel/proto_model.v
theories/channel/proto_channel.v
......
......@@ -17,8 +17,9 @@ and [chan_own]:
[s] ([Left] or [Right]) has contents [vs]. *)
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.heap_lang Require Import lifting.
From iris.algebra Require Import excl auth list.
From actris.utils Require Import auth_excl llist misc.
From actris.utils Require Import auth_excl llist.
Set Default Proof Using "Type".
Inductive side := Left | Right.
......
From iris.heap_lang Require Import notation.
Set Default Proof Using "Type".
(** MOVE TO IRIS *)
Global Instance fst_atomic a v1 v2 : Atomic a (Fst (v1,v2)%V).
Proof.
apply strongly_atomic_atomic, ectx_language_atomic;
[inversion 1; naive_solver
|apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
Qed.
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