Delaying the continuation makes bounds checks precede copying and hashing
in a strict native realization, as well as in the lazy checker.
54def regionFrameRequire =
55 (lambda unrestricted flag : Nat .
56 (lambda unrestricted code : (family RegionFrameFailure) .
57 (lambda unrestricted next : (pi unrestricted unit : Nat . (family StdResult (family RegionFrameFailure) Bytes)) .
58 (nat-eliminate
59 (lambda unrestricted n : Nat . (family StdResult (family RegionFrameFailure) Bytes))
60 (regionFrameFailure code)
61 (lambda unrestricted p : Nat .
62 (lambda unrestricted ignored : (family StdResult (family RegionFrameFailure) Bytes) .
63 (next 0)))
64 flag))))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.