vstd::laws_eq

Function obeys_eq_spec_properties

Source 
pub open spec fn obeys_eq_spec_properties<T: PartialEq>() -> bool
Expand description
{
    &&& forall |x: T, y: T| #[trigger] x.eq_spec(&y) <==> y.eq_spec(&x)
    &&& forall |x: T, y: T, z: T| {
        x.eq_spec(&y) && #[trigger] y.eq_spec(&z) ==> #[trigger] x.eq_spec(&z)
    }

}