"value < 2^bits" WITHOUT building 2^bits: halve bits times and ask whether
anything is left. The general form of naturalBelowBytePower (a byte is eight
halvings); it is what a limit such as "fits int64" (bits = 63) or "at most
16 MiB of input" (bits = 24) must use at runtime, since 2^24 alone costs
2.75 GB to materialise and 2^63 cannot be materialised at all.
252def naturalBelowTwoPower =
253 (lambda unrestricted bits : Nat .
254 (lambda unrestricted value : Nat .
255 (naturalIsZero
256 (nat-eliminate
257 (lambda unrestricted current : Nat . Nat)
258 value
259 (lambda unrestricted predecessor : Nat .
260 (lambda unrestricted quotient : Nat .
261 (naturalDivideUnchecked quotient (succ (succ zero)))))
262 bits))))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.