---- (C): every span in a window lies in one named range ----
1169def deviceArenaWithin =
1170 (lambda unrestricted residents : (family ArenaResidents) .
1171 (lambda unrestricted low : Nat .
1172 (lambda unrestricted high : Nat .
1173 (eliminate
1174 ArenaResidents
1175 (lambda unrestricted current : (family ArenaResidents) . Nat)
1176 residents
1177 (branch ArenaResidentsEnd . 0)
1178 (branch
1179 ArenaResidentsNext
1180 head
1181 tail
1182 induction
1183 .
1184 (naturalOr
1185 (naturalAnd (deviceArenaContains head low) (deviceArenaContains head high))
1186 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.