Skip to content

Commit

Permalink
Import apply_closure into kani_core (#3375)
Browse files Browse the repository at this point in the history
This enables use of `|result|` when verifying the standard library.
  • Loading branch information
tautschnig committed Jul 24, 2024
1 parent 5a5044a commit 1b1a9b6
Showing 1 changed file with 7 additions and 0 deletions.
7 changes: 7 additions & 0 deletions library/kani_core/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
}
};
}

0 comments on commit 1b1a9b6

Please sign in to comment.