From 78d4709cb3d686c4befb8c153443bf9f7a5c60d7 Mon Sep 17 00:00:00 2001
From: Jay Bosamiya <jaybosamiya@gmail.com>
Date: Mon, 19 Feb 2024 12:44:55 -0500
Subject: [PATCH] Update to latest syntax.rs

---
 examples/syntax.rs | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/examples/syntax.rs b/examples/syntax.rs
index 038a7ef..e7bbd68 100644
--- a/examples/syntax.rs
+++ b/examples/syntax.rs
@@ -560,6 +560,22 @@ proof fn uses_is(t: ThisOrThat) {
     }
 }
 
+proof fn uses_arrow_matches_1(t: ThisOrThat)
+    requires
+        t is That ==> t->v == 3,
+        t is This ==> t->0 == 4,
+{
+    assert(t matches ThisOrThat::This(k) ==> k == 4);
+    assert(t matches ThisOrThat::That { v } ==> v == 3);
+}
+
+proof fn uses_arrow_matches_2(t: ThisOrThat)
+    requires
+        t matches ThisOrThat::That { v: a } && a == 3,
+{
+    assert(t is That && t->v == 3);
+}
+
 #[verifier::external_body]
 struct Collection {}