From f50f5d4dbc66c58032bb3f8e76c10e21496db0a0 Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@cmu.edu>
Date: Tue, 13 Feb 2024 09:03:06 -0500
Subject: [PATCH] Add a test

---
 tests/verus-consistency.rs | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
index 155d350..3415a71 100644
--- 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!
     "###);
 }