[a, a+n) and [b, b+m) are disjoint when one ends before the other begins.
94def arenaDisjoint =
95 (lambda unrestricted left : (family ArenaResident) .
96 (lambda unrestricted right : (family ArenaResident) .
97 (naturalOr
98 (naturalLessOrEqual (arenaResidentEndOf left) (arenaResidentOffsetOf right))
99 (naturalLessOrEqual (arenaResidentEndOf right) (arenaResidentOffsetOf left)))))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.