extern_spec_std_cmp_min

creusot_contracts::std::cmp

Function extern_spec_std_cmp_min 

Source 
pub fn extern_spec_std_cmp_min<T>(v1: T, v2: T) -> T
where
    T: Ord + DeepModel,
    T::DeepModelTy: OrdLogic,
Expand description

extern spec for ::std::cmp::min<T>

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

ensures 

result.deep_model() <= v1.deep_model()

ensures 

result.deep_model() <= v2.deep_model()

ensures 

result == v1 || result == v2

ensures 

v1.deep_model() < v2.deep_model() ==> result == v1

ensures 

v2.deep_model() <= v1.deep_model() ==> result == v2