diff --git a/tests/atomic.v b/tests/atomic.v index fc69d02d080379a2290a37de9737e6cd345e21d4..e00a871bcd40451da007994060e66e2127dc2d73 100644 --- a/tests/atomic.v +++ b/tests/atomic.v @@ -1,3 +1,6 @@ +Require Import stdpp.coPset. +Require Import iris.bi.telescopes. +Require Import iris.bi.lib.atomic. From iris.proofmode Require Import tactics. From iris.program_logic Require Export atomic. From iris.heap_lang Require Import proofmode notation atomic_heap. @@ -5,6 +8,14 @@ From iris.prelude Require Import options. Unset Mangle Names. +Section definition. + Context `{BiFUpd PROP} {TA TB : tele} (Eo Ei : coPset). + + Definition AU_tele_quantify_iris : Prop := + ⊢ ∀ (TA TB : tele) (α : TA → PROP) (β Φ : TA → TB → PROP), + atomic_update Eo Ei α β Φ. +End definition. + Section tests. Context `{!heapGS Σ} {aheap: atomic_heap Σ}. Import atomic_heap.notation.