Add support for lifetime_param

examples/wip.rs

@@ -1,20 +1,8 @@
 verus! {
 
-struct StrictlyOrderedVec<K: KeyTrait> {
-    a: int,
+fn get<'a>(&'a self) -> (o: Option<&'a V>) {
+    a
 }
 
-struct DelegationMap<
-    #[verifier(maybe_negative)]
-    K: KeyTrait + VerusClone,
-> {
-    b: int,
-}
-
-impl<K: KeyTrait + VerusClone> DelegationMap<K> {
-    fn view() -> Map<K, AbstractEndPoint> {
-        c
-    }
-}
 
 } // verus!

src/lib.rs

@@ -666,7 +666,7 @@ fn to_doc<'a>(
         Rule::generic_param => map_to_doc(ctx, arena, pair),
         Rule::type_param => map_to_doc(ctx, arena, pair),
         Rule::const_param => unsupported(pair),
-        Rule::lifetime_param => unsupported(pair),
+        Rule::lifetime_param => map_to_doc(ctx, arena, pair),
         Rule::where_clause => unsupported(pair),
         Rule::where_pred => unsupported(pair),
         Rule::visibility => s.append(arena.space()),

tests/snap-tests.rs

@@ -808,3 +808,26 @@ pub fn clone_vec_u8() {
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_lifetimes() {
+    let file = r#"
+verus! {
+
+fn get<'a>(&'a self, k: &K) -> (o: Option<&'a V>) {
+    a
+}
+
+} // verus!
+"#;
+
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    fn get<'a>(&'aself, k: &K) -> (o: Option<&'aV>) {
+        a
+    }
+
+    } // verus!
+    "###);
+}