Source/Packages

Runtime.DeviceArenaCertificate

packages/execution/src/Runtime/DeviceArenaCertificate.alpha

1,800 lines133 declarations66.8 KiBSHA-256 74ef7fffbf20

def · lines 1188–1207

deviceArenaMeets

Full file
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.