1 when `resident` was declared, in the same place, and nothing has been
declared over it since
1260def deviceArenaIntact =
1261 (lambda unrestricted tracked : (family DeviceArenaTracked) .
1262 (lambda unrestricted resident : (family ArenaResident) .
1263 (eliminate
1264 DeviceArenaTracked
1265 (lambda unrestricted current : (family DeviceArenaTracked) . Nat)
1266 tracked
1267 (branch DeviceArenaTrackedEnd . 0)
1268 (branch
1269 DeviceArenaTrackedNext
1270 head
1271 clobbered
1272 tail
1273 induction
1274 .
1275 (nat-eliminate
1276 (lambda unrestricted same : Nat . Nat)
1277 induction
1278 (lambda unrestricted p : Nat .
1279 (lambda unrestricted ignored : Nat .
1280 (naturalAnd
1281 (naturalIsZero clobbered)
1282 (naturalAnd
1283 (naturalEqual (arenaResidentOffsetOf head) (arenaResidentOffsetOf resident))
1284 (naturalEqual (arenaResidentEndOf head) (arenaResidentEndOf resident))))))
1285 (bytes-equal (deviceArenaResidentIdentity head) (deviceArenaResidentIdentity resident)))))))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.