1 when a resident of this name is among `residents`
1304def deviceArenaAnyNamed =
1305 (lambda unrestricted residents : (family ArenaResidents) .
1306 (lambda unrestricted resident : (family ArenaResident) .
1307 (eliminate
1308 ArenaResidents
1309 (lambda unrestricted current : (family ArenaResidents) . Nat)
1310 residents
1311 (branch ArenaResidentsEnd . 0)
1312 (branch
1313 ArenaResidentsNext
1314 head
1315 tail
1316 induction
1317 .
1318 (naturalOr
1319 (bytes-equal (deviceArenaResidentIdentity head) (deviceArenaResidentIdentity resident))
1320 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.