requires

Attribute Macro requires 

Source
#[requires]
Expand description

Pre-conditions are checked before the function body is run.

ยงExample

#[requires(elems.len() >= 1)]
fn max<T: Ord + Copy>(elems: &[T]) -> T {
   // ...
}