Unverified Commit 09b6a0c3 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Add testcase for #461

parent de41b20f
Pipeline #66060 failed with stage
in 6 minutes and 24 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