extern_spec_std_cmp_Ord_cmp

creusot_contracts::std::cmp

Function extern_spec_std_cmp_Ord_cmp 

Source 
pub fn extern_spec_std_cmp_Ord_cmp<Self_>(
    self_: &Self_,
    rhs: &Self_,
) -> Ordering
where
    Self_: DeepModel + ?Sized + Ord,
    Self_::DeepModelTy: OrdLogic,
Expand description

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

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

ensures 

result == (*self).deep_model().cmp_log((*rhs).deep_model())