Unverified Commit 8aa6d9eb authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Add testcase for #461

parent 5c6621c2
Pipeline #66095 canceled with stage
in 9 seconds
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