Commit 78d94a8a authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'sbi-eq-notation-sections' into 'master'

sbi_internal_eq: add "sections" of notation, following stdpp

See merge request iris/iris!404
parents ab3b5c77 e5a2bcff
......@@ -5,6 +5,10 @@ Section tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Lemma type_sbi_internal_eq_annot P :
P @{PROP} P (@{PROP}) P P (P .) P (. P) P.
Proof. done. Qed.
Lemma test_eauto_emp_isplit_biwand P : emp P - P.
Proof. eauto 6. Qed.
......
......@@ -290,6 +290,12 @@ Notation "∃ x .. y , P" :=
Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
Infix "≡" := sbi_internal_eq : bi_scope.
Infix "≡@{ A }" := (sbi_internal_eq (A := A)) (only parsing) : bi_scope.
Notation "( X ≡.)" := (sbi_internal_eq X) (only parsing) : bi_scope.
Notation "(.≡ X )" := (λ Y, Y X)%I (only parsing) : bi_scope.
Notation "(≡@{ A } )" := (sbi_internal_eq (A := A)) (only parsing) : bi_scope.
Notation "▷ P" := (sbi_later P) : bi_scope.
Definition bi_emp_valid {PROP : bi} (P : PROP) : Prop := emp P.
......
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