extern_spec_std_cmp_PartialOrd_Rhs_ge

creusot_contracts::std::cmp

Function extern_spec_std_cmp_PartialOrd_Rhs_ge 

Source 
pub fn extern_spec_std_cmp_PartialOrd_Rhs_ge<Self_, Rhs>(
    self_: &Self_,
    other: &Rhs,
) -> bool
where
    Self_: DeepModel + ?Sized + PartialOrd<Rhs>,
    Rhs: DeepModel<DeepModelTy = Self_::DeepModelTy>,
    Self_::DeepModelTy: OrdLogic,
Expand description

extern spec for ::std::cmp::PartialOrd::ge

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

ensures 

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