vstd::laws_cmp

Function obeys_cmp_spec

Source 
pub open spec fn obeys_cmp_spec<T: Ord>() -> bool
Expand description
{
    &&& obeys_eq_spec::<T>()
    &&& obeys_cmp_partial_ord::<T>()
    &&& obeys_cmp_ord::<T>()
    &&& obeys_partial_cmp_spec_properties::<T>()

}