Skip to main content

extern_spec_T__slice_T_binary_search

creusot_std::std::slice

Function extern_spec_T__slice_T_binary_search 

Source 
pub fn extern_spec_T__slice_T_binary_search<T>(
    self_: &[T],
    x: &T,
) -> Result<usize, usize>
where
    T: Ord + DeepModel,
    T::DeepModelTy: OrdLogic,
Expand description

extern spec for slice<T>::binary_search

This is not a real function: its only use is for documentation.

requires 

self

ensures 

self

ensures

self@.len() &&
forall<j> 0 <= j && j < self@.len() ==> self

ensures 

self

ensures 

self@.len() ==> x.deep_model() < self