offset mod alignment = 0, extent > 0, alignment > 0, offset + extent <= arena
69def arenaResidentValid =
70 (lambda unrestricted arenaExtent : Nat .
71 (lambda unrestricted resident : (family ArenaResident) .
72 (eliminate ArenaResident (lambda unrestricted current : (family ArenaResident) . Nat) resident
73 (branch ArenaResidentValue identity offset extent alignment .
74 (naturalAnd
75 (naturalIsZero (naturalIsZero alignment))
76 (naturalAnd
77 (naturalIsZero (nat-modulo offset alignment))
78 (naturalAnd
79 (naturalIsZero (naturalIsZero extent))
80 (naturalLessOrEqual (naturalAdd offset extent) arenaExtent))))))))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.