Commit fda69eb6 authored by Hai Dang's avatar Hai Dang
Browse files

Minor cleanup of imports

parent e5093c03
Require Import stdpp.namespaces.
Require Import iris.bi.telescopes.
From iris.proofmode Require Import proofmode classes.
From iris.proofmode Require Import proofmode.
Require Export iris.bi.lib.atomic.
Require Export gpfsl.base_logic.weakestpre.
Require Import gpfsl.logic.invariants.
Require Import iris.prelude.options.
Definition atomic_wp `{!noprolG Σ} {TA TB : tele}
(e: expr) (* expression *)
(tid : thread_id)
......@@ -19,7 +21,7 @@ Definition atomic_wp `{!noprolG Σ} {TA TB : tele}
(Φ : val vProp Σ),
(* Fix the inner mask to the shared global namespace histN *)
atomic_update (E) (histN) α β (λ.. x y, POST x y - Φ (f x y)) -
WP e @ tid ; top {{ Φ }}.
WP e @ tid ; {{ Φ }}.
Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ tid ; E '<<<' ∃ y1 .. yn , β , 'RET' v , POST '>>>'" :=
(atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
......
From iris.program_logic Require Import weakestpre.
From iris.proofmode Require Import proofmode.
From gpfsl.lang Require Export notation.
......
Markdown is supported
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