Expand description
A lexicographically ordered pair of timestamps.
Two timestamps (s1, t1) and (s2, t2) are ordered either if s1 and s2 are ordered, or if s1 equals s2 and t1 and t2 are ordered.
The join of two timestamps should have as its first coordinate the join of the first coordinates, and for its second coordinate the join of the second coordinates for elements whose first coordinate equals the computed join. That may be the minimum element of the second lattice, if neither first element equals the join.
Structsยง
- A pair of timestamps, partially ordered by the product order.