Support generic argument binding

Useful for associated type constraints, such as `trait Foo<T>: Bar<V = Baz<T>>`

CHANGELOG.md

@@ -1,5 +1,8 @@
 # Unreleased
 
+* Support generic argument binding
+  - Useful for associated type constraints, such as `trait Foo<T>: Bar<V = Baz<T>>`
+
 # v0.3.0
 
 * Support attributes on `broadcast group` items

src/lib.rs

@@ -793,6 +793,7 @@ fn to_doc<'a>(
         Rule::assoc_type_arg => unsupported(pair),
         Rule::lifetime_arg => map_to_doc(ctx, arena, pair),
         Rule::const_arg => unsupported(pair),
+        Rule::generic_args_binding => map_to_doc(ctx, arena, pair),
         Rule::macro_call => s,
         Rule::macro_call_stmt => s,
         Rule::punctuation => map_to_doc(ctx, arena, pair),

src/verus.pest

@@ -453,7 +453,8 @@ generic_arg_list_with_colons = {
 }
 
 generic_arg = {
-    type_arg
+    generic_args_binding
+  | type_arg
   | assoc_type_arg
   | lifetime_arg
   | const_arg
@@ -477,6 +478,10 @@ const_arg = {
     expr
 }
 
+generic_args_binding = {
+    identifier ~ eq_str ~ type
+}
+
 // TODO: Special handling for the calc! and state_machine! macros?
 macro_call = {
     attr* ~ path ~ bang_str ~ !"=" ~ token_tree

tests/verus-consistency.rs

@@ -2094,3 +2094,22 @@ proof fn b()
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_generic_arg_binding() {
+    let file = r###"
+verus! {
+pub trait Foo<T>: View<V = Seq<T>> {
+}
+} // verus!
+"###;
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    pub trait Foo<T>: View<V = Seq<T>> {
+
+    }
+
+    } // verus!
+    "###);
+}