Allow patterns and type annotations in propset notation

stdpp/propset.v

@@ -7,7 +7,7 @@ Add Printing Constructor propset.
 Global Arguments PropSet {_} _ : assert.
 Global Arguments propset_car {_} _ _ : assert.
 Notation "{[ x | P ]}" := (PropSet (λ x, P))
-  (at level 1, format "{[  x  |  P  ]}") : stdpp_scope.
+  (at level 1, x at level 200 as pattern, format "{[  x  |  P  ]}") : stdpp_scope.
 
 Global Instance propset_elem_of {A} : ElemOf A (propset A) := λ x X, propset_car X x.
 

tests/propset.v

+From stdpp Require Import propset.
+
+Lemma diagonal : {[ (a,b) : nat * nat | a = b ]} ≡ (λ x, (x,x)) <$> ⊤.
+Proof. set_unfold. intros []. naive_solver. Qed.
+
+Lemma diagonal2 : {[ (a,b) | a =@{nat} b ]} ≡ {[ x | x.1 = x.2 ]}.
+Proof. set_unfold. intros []. naive_solver. Qed.
+
+Lemma simple_pattern_does_not_match : {[ x : nat | x = x]} = PropSet (λ x, x = x).
+Proof. exact eq_refl. Qed.