From 5e8df0463581a1a685d078392657f6d7743269b7 Mon Sep 17 00:00:00 2001
From: Chris Hawblitzel <Chris.Hawblitzel@microsoft.com>
Date: Wed, 5 Feb 2025 21:59:09 -0800
Subject: [PATCH] Fix syn parsing's continue_parsing_early for assert/proof

---
 dependencies/syn/src/classify.rs | 4 ++--
 dependencies/syn/src/expr.rs     | 6 ++++++
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/dependencies/syn/src/classify.rs b/dependencies/syn/src/classify.rs
index 9d069d2fec..440ac67c20 100644
--- a/dependencies/syn/src/classify.rs
+++ b/dependencies/syn/src/classify.rs
@@ -34,8 +34,8 @@ pub(crate) fn requires_comma_to_be_match_arm(expr: &Expr) -> bool {
         | Expr::Const(_) => false,
 
         // verus
-        | Expr::Assert(e) => e.body.is_none(),
-        | Expr::AssertForall(_) => false,
+        Expr::Assert(e) => e.body.is_none(),
+        Expr::AssertForall(_) => false,
         Expr::Assume(_)
         | Expr::RevealHide(_)
         | Expr::View(_)
diff --git a/dependencies/syn/src/expr.rs b/dependencies/syn/src/expr.rs
index 65fe66b25d..e99938c3e5 100644
--- a/dependencies/syn/src/expr.rs
+++ b/dependencies/syn/src/expr.rs
@@ -2313,6 +2313,12 @@ pub(crate) mod parsing {
             | Expr::Unsafe(_)
             | Expr::Const(_)
             | Expr::Block(_) => false,
+
+            // verus
+            Expr::Assert(e) => e.body.is_none(),
+            Expr::AssertForall(_) => false,
+            Expr::Unary(e) if matches!(e.op, crate::op::UnOp::Proof(_)) => false,
+
             _ => true,
         }
     }