AlphaGitHub
Source/Packages

Runtime.DeviceArenaCertificate

packages/execution/src/Runtime/DeviceArenaCertificate.alpha

1,800 lines133 declarations66.8 KiBSHA-256 74ef7fffbf20
Download exact fileView at revisionf5034773ad4bb52133

def · lines 194–208

deviceArenaAnyContains

Full file
194def deviceArenaAnyContains =
195  (lambda unrestricted residents : (family ArenaResidents) .
196    (lambda unrestricted address : Nat .
197      (eliminate
198        ArenaResidents
199        (lambda unrestricted current : (family ArenaResidents) . Nat)
200        residents
201        (branch ArenaResidentsEnd . 0)
202        (branch
203          ArenaResidentsNext
204          head
205          tail
206          induction
207          .
208          (naturalOr (deviceArenaContains head address) 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.