Update to latest syntax.rs

verus-lang · Feb 19, 2024 · 78d4709 · 78d4709
1 parent 11e6b89
commit 78d4709
Showing 1 changed file with 16 additions and 0 deletions.
diff --git 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 {}