extern_spec_std_cmp_max

creusot_contracts::std::cmp

Function extern_spec_std_cmp_max 

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

extern spec for ::std::cmp::max<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 == v2

ensures 

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