A disjoint intersection is an empty interval at the larger begin. Preserve
begin <= end so downstream consumers can reuse the ordinary interval laws.
46def intervalIntersection =
47 (lambda unrestricted left : (family LogicalInterval) .
48 (lambda unrestricted right : (family LogicalInterval) .
49 (let unrestricted begin =
50 (naturalSelect
51 (naturalLess (intervalBegin left) (intervalBegin right))
52 (intervalBegin right)
53 (intervalBegin left))
54 in
55 (let unrestricted end =
56 (naturalMinimum (intervalEnd left) (intervalEnd right))
57 in
58 (constructor
59 LogicalInterval
60 LogicalIntervalOf
61 begin
62 (naturalSelect (naturalLess end begin) begin end))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.