extern_spec_std_cmp_Ord_min

creusot_contracts::std::cmp

Function extern_spec_std_cmp_Ord_min 

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

extern spec for ::std::cmp::Ord::min

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 == self

ensures 

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