1188def deviceArenaMeets =
1189 (lambda unrestricted windows : (family ArenaResidents) .
1190 (lambda unrestricted low : Nat .
1191 (lambda unrestricted high : Nat .
1192 (eliminate
1193 ArenaResidents
1194 (lambda unrestricted current : (family ArenaResidents) . Nat)
1195 windows
1196 (branch ArenaResidentsEnd . 0)
1197 (branch
1198 ArenaResidentsNext
1199 head
1200 tail
1201 induction
1202 .
1203 (naturalOr
1204 (naturalAnd
1205 (naturalLess low (arenaResidentEndOf head))
1206 (naturalLessOrEqual (arenaResidentOffsetOf head) high))
1207 induction))))))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.