Commit 56e9d264 authored by Ralf Jung's avatar Ralf Jung
Browse files

cleanup imports

parent 9dd4d1ea
Pipeline #66210 passed with stage
in 20 minutes and 15 seconds
Require Import stdpp.coPset.
Require Import
Require Import
From Require Import atomic.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Import proofmode notation atomic_heap.
......@@ -11,6 +9,8 @@ Unset Mangle Names.
Section definition.
Context `{BiFUpd PROP} {TA TB : tele} (Eo Ei : coPset).
(** We can quantify over telescopes *inside* Iris and use them with atomic
updates. *)
Definition AU_tele_quantify_iris : Prop :=
(TA TB : tele) (α : TA PROP) (β Φ : TA TB PROP),
atomic_update Eo Ei α β Φ.
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