Add a test

verus-lang · Feb 13, 2024 · f50f5d4 · f50f5d4
1 parent 54bf294
commit f50f5d4
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
@@ -788,6 +788,14 @@ trait KeyTrait: Sized {
     fn zero_spec() -> Self where Self: std::marker::Sized;
 }
 
+spec fn map(f: spec_fn(A) -> B) {
+    1
+}
+
+spec fn adder(x: int) -> spec_fn(int) -> int {
+    |y: int| x + y
+}
+
 }
 "#;
 
@@ -809,6 +817,14 @@ trait KeyTrait: Sized {
         fn zero_spec() -> Self where Self: std::marker::Sized;
     }
 
+    spec fn map(f: spec_fn(A) -> B) {
+        1
+    }
+
+    spec fn adder(x: int) -> spec_fn(int) -> int {
+        |y: int| x + y
+    }
+
     } // verus!
     "###);
 }