From db05f07decabe60bdd0c799356bd24f666770be8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thibaut=20P=C3=A9rami?= <thibaut.perami@cl.cam.ac.uk>
Date: Wed, 18 Oct 2023 11:41:37 +0100
Subject: [PATCH] Allow patterns and type annotations in propset notation
---
stdpp/propset.v | 2 +-
tests/propset.ref | 0
tests/propset.v | 10 ++++++++++
3 files changed, 11 insertions(+), 1 deletion(-)
create mode 100644 tests/propset.ref
create mode 100644 tests/propset.v
diff --git a/stdpp/propset.v b/stdpp/propset.v
index 1ed3af52..5c829eb6 100644
--- a/stdpp/propset.v
+++ b/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.
diff --git a/tests/propset.ref b/tests/propset.ref
new file mode 100644
index 00000000..e69de29b
diff --git a/tests/propset.v b/tests/propset.v
new file mode 100644
index 00000000..64a21059
--- /dev/null
+++ b/tests/propset.v
@@ -0,0 +1,10 @@
+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.
--
GitLab