From 1b1a9b6714038382bc9a592da056dd202e57d8e4 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 24 Jul 2024 17:53:45 +0200
Subject: [PATCH] Import apply_closure into kani_core (#3375)

This enables use of `|result|` when verifying the standard library.
---
 library/kani_core/src/lib.rs | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index 68a8e79658f1..a07ba7ca8ec4 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -384,6 +384,13 @@ macro_rules! kani_intrinsics {
             #[doc(hidden)]
             #[rustc_diagnostic_item = "KaniInitContracts"]
             pub fn init_contracts() {}
+
+            /// This should only be used within contracts. The intent is to
+            /// perform type inference on a closure's argument
+            #[doc(hidden)]
+            pub fn apply_closure<T, U: Fn(&T) -> bool>(f: U, x: &T) -> bool {
+                f(x)
+            }
         }
     };
 }