vstd::laws_cmp

Function obeys_cmp_partial_ord

Source 
pub open spec fn obeys_cmp_partial_ord<T: PartialOrd>() -> bool
Expand description
{
    &&& T::obeys_eq_spec()
    &&& T::obeys_partial_cmp_spec()
    &&& forall |x: T, y: T| {
        x.eq_spec(&y) <==> x.partial_cmp_spec(&y) == Some(Ordering::Equal)
    }

}