Skip to content
Snippets Groups Projects
Commit a3cc36e4 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso Committed by Robbert Krebbers
Browse files

Fix scopes of bupd and fupd

parent e2c87974
No related branches found
No related tags found
No related merge requests found
......@@ -6,6 +6,10 @@ Section base_logic_tests.
Context {M : ucmraT}.
Implicit Types P Q R : uPred M.
(* Test scopes for bupd *)
Definition use_bupd_uPred (n : nat) : uPred M :=
|==> m : nat , n = 2 ⌝.
Lemma test_random_stuff (P1 P2 P3 : nat uPred M) :
(x y : nat) a b,
x y
......@@ -52,6 +56,12 @@ Section iris_tests.
Context `{!invG Σ, !cinvG Σ, !na_invG Σ}.
Implicit Types P Q R : iProp Σ.
(* Test scopes for bupd and fupd *)
Definition use_bupd_iProp (n : nat) : iProp Σ :=
|==> m : nat , n = 2 ⌝.
Definition use_fupd_iProp (n : nat) : iProp Σ :=
|={}=> m : nat , n = 2 ⌝.
Lemma test_masks N E P Q R :
N E
(True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ Q ={E}=∗ R.
......
......@@ -7,6 +7,7 @@ bundle these operational type classes with the laws. *)
Class BUpd (PROP : Type) : Type := bupd : PROP PROP.
Instance : Params (@bupd) 2 := {}.
Hint Mode BUpd ! : typeclass_instances.
Arguments bupd {_}%type_scope {_} _%bi_scope.
Notation "|==> Q" := (bupd Q) : bi_scope.
Notation "P ==∗ Q" := (P |==> Q) (only parsing) : stdpp_scope.
......@@ -15,6 +16,7 @@ Notation "P ==∗ Q" := (P -∗ |==> Q)%I : bi_scope.
Class FUpd (PROP : Type) : Type := fupd : coPset coPset PROP PROP.
Instance: Params (@fupd) 4 := {}.
Hint Mode FUpd ! : typeclass_instances.
Arguments fupd {_}%type_scope {_} _ _ _%bi_scope.
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I : bi_scope.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment