Skip to content
Snippets Groups Projects
Commit 316257fb authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'robbert/siProp_scope' into 'master'

Dump `siProp_scope` and use `bi_scope`. This is consistent with `uPred`.

See merge request iris/iris!786
parents 456db30e b034fd49
No related branches found
No related tags found
No related merge requests found
...@@ -435,6 +435,8 @@ Implicit Types A : Type. ...@@ -435,6 +435,8 @@ Implicit Types A : Type.
Local Arguments uPred_holds {_} !_ _ _ /. Local Arguments uPred_holds {_} !_ _ _ /.
Local Hint Immediate uPred_in_entails : core. Local Hint Immediate uPred_in_entails : core.
(** The notations below are implicitly local due to the section, so we do not
mind the overlap with the general BI notations. *)
Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I) : stdpp_scope. Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I) : stdpp_scope.
Notation "(⊢)" := (@uPred_entails M) (only parsing) : stdpp_scope. Notation "(⊢)" := (@uPred_entails M) (only parsing) : stdpp_scope.
Notation "P ⊣⊢ Q" := (@uPred_equiv M P%I Q%I) : stdpp_scope. Notation "P ⊣⊢ Q" := (@uPred_equiv M P%I Q%I) : stdpp_scope.
......
...@@ -13,9 +13,7 @@ Local Coercion siProp_holds : siProp >-> Funclass. ...@@ -13,9 +13,7 @@ Local Coercion siProp_holds : siProp >-> Funclass.
Global Arguments siProp_holds : simpl never. Global Arguments siProp_holds : simpl never.
Add Printing Constructor siProp. Add Printing Constructor siProp.
Declare Scope siProp_scope. Bind Scope bi_scope with siProp.
Delimit Scope siProp_scope with SI.
Bind Scope siProp_scope with siProp.
Section cofe. Section cofe.
Inductive siProp_equiv' (P Q : siProp) : Prop := Inductive siProp_equiv' (P Q : siProp) : Prop :=
...@@ -130,17 +128,21 @@ Ltac unseal := rewrite !unseal_eqs /=. ...@@ -130,17 +128,21 @@ Ltac unseal := rewrite !unseal_eqs /=.
Section primitive. Section primitive.
Local Arguments siProp_holds !_ _ /. Local Arguments siProp_holds !_ _ /.
(** The notations below are implicitly local due to the section, so we do not
mind the overlap with the general BI notations. *)
Notation "P ⊢ Q" := (siProp_entails P Q). Notation "P ⊢ Q" := (siProp_entails P Q).
Notation "'True'" := (siProp_pure True) : siProp_scope. Notation "'True'" := (siProp_pure True) : bi_scope.
Notation "'False'" := (siProp_pure False) : siProp_scope. Notation "'False'" := (siProp_pure False) : bi_scope.
Notation "'⌜' φ '⌝'" := (siProp_pure φ%type%stdpp) : siProp_scope. Notation "'⌜' φ '⌝'" := (siProp_pure φ%type%stdpp) : bi_scope.
Infix "∧" := siProp_and : siProp_scope. Infix "∧" := siProp_and : bi_scope.
Infix "∨" := siProp_or : siProp_scope. Infix "∨" := siProp_or : bi_scope.
Infix "→" := siProp_impl : siProp_scope. Infix "→" := siProp_impl : bi_scope.
Notation "∀ x .. y , P" := (siProp_forall (λ x, .. (siProp_forall (λ y, P%SI)) ..)) : siProp_scope. Notation "∀ x .. y , P" :=
Notation "∃ x .. y , P" := (siProp_exist (λ x, .. (siProp_exist (λ y, P%SI)) ..)) : siProp_scope. (siProp_forall (λ x, .. (siProp_forall (λ y, P%I)) ..)) : bi_scope.
Notation "x ≡ y" := (siProp_internal_eq x y) : siProp_scope. Notation "∃ x .. y , P" :=
Notation "▷ P" := (siProp_later P) (at level 20, right associativity) : siProp_scope. (siProp_exist (λ x, .. (siProp_exist (λ y, P%I)) ..)) : bi_scope.
Notation "x ≡ y" := (siProp_internal_eq x y) : bi_scope.
Notation "▷ P" := (siProp_later P) : bi_scope.
(** Below there follow the primitive laws for [siProp]. There are no derived laws (** Below there follow the primitive laws for [siProp]. There are no derived laws
in this file. *) in this file. *)
......
From iris.si_logic Require Import bi.
(** Make sure that [siProp]s are parsed in [bi_scope]. *)
Definition test : siProp := True.
Definition testI : siPropI := True.
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