Unverified Commit 9851ef8d authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Add testcase for #461

parent e60de03f
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.
Supports Markdown
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