vstd::laws_cmp

Function obeys_cmp_ord

Source 
pub open spec fn obeys_cmp_ord<T: Ord>() -> bool
Expand description
{
    &&& T::obeys_cmp_spec()
    &&& forall |x: T, y: T| x.partial_cmp_spec(&y) == Some(x.cmp_spec(&y))

}