vstd::laws_cmp

Function obeys_partial_cmp_spec_properties

Source 
pub open spec fn obeys_partial_cmp_spec_properties<T: PartialOrd>() -> bool
Expand description
{
    &&& forall |x: T, y: T| {
        #[trigger] x.partial_cmp_spec(&y) == Some(Ordering::Equal) <==> x.eq_spec(&y)
    }
    &&& forall |x: T, y: T| {
        #[trigger] x.partial_cmp_spec(&y) == Some(Ordering::Less)
            <==> y.partial_cmp_spec(&x) == Some(Ordering::Greater)
    }
    &&& forall |x: T, y: T, z: T| {
        x.partial_cmp_spec(&y) == Some(Ordering::Less)
            && #[trigger] y.partial_cmp_spec(&z) == Some(Ordering::Less)
            ==> #[trigger] x.partial_cmp_spec(&z) == Some(Ordering::Less)
    }
    &&& forall |x: T, y: T, z: T| {
        x.partial_cmp_spec(&y) == Some(Ordering::Greater)
            && #[trigger] y.partial_cmp_spec(&z) == Some(Ordering::Greater)
            ==> #[trigger] x.partial_cmp_spec(&z) == Some(Ordering::Greater)
    }
    &&& obeys_eq_spec_properties::<T>()

}