extern_spec_std_cmp_Ord_max

creusot_contracts::std::cmp

Function extern_spec_std_cmp_Ord_max 

Source 
pub fn extern_spec_std_cmp_Ord_max<Self_>(self_: Self_, o: Self_) -> Self_
where
    Self_: Sized + DeepModel + ?Sized + Ord,
    Self_::DeepModelTy: OrdLogic,
Expand description

extern spec for ::std::cmp::Ord::max

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

ensures 

result.deep_model() >= self.deep_model()

ensures 

result.deep_model() >= o.deep_model()

ensures 

result == self || result == o

ensures 

self.deep_model() <= o.deep_model() ==> result == o

ensures 

o.deep_model() < self.deep_model() ==> result == self