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

Add ∗-∗ as notation in stdpp_scope similar to -∗.

parent 7e865892
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/bi/derived_connectives.v
+ 1
− 0
View file @ 3c8525f8
...@@ -12,6 +12,7 @@ Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP := ...@@ -12,6 +12,7 @@ Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
Global Arguments bi_wand_iff {_} _%I _%I : simpl never. Global Arguments bi_wand_iff {_} _%I _%I : simpl never.
Global Instance: Params (@bi_wand_iff) 1 := {}. Global Instance: Params (@bi_wand_iff) 1 := {}.
Infix "∗-∗" := bi_wand_iff : bi_scope. Infix "∗-∗" := bi_wand_iff : bi_scope.
Notation "P ∗-∗ Q" := (⊢ P ∗-∗ Q) : stdpp_scope.
Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P. Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
Global Arguments Persistent {_} _%I : simpl never. Global Arguments Persistent {_} _%I : simpl never.
......
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