Keep scalar arithmetic bounded while consuming the complete malformed escape.
536def quotedAppendBoundedHexDigit =
537 (lambda unrestricted count : Nat .
538 (lambda unrestricted accumulator : (family ModelWord32) .
539 (lambda unrestricted digit : Nat .
540 (nat-eliminate
541 (lambda unrestricted condition : Nat . (family ModelWord32))
542 accumulator
543 (lambda unrestricted predecessor : Nat .
544 (lambda unrestricted unused : (family ModelWord32) .
545 (quotedAppendHexDigit accumulator digit)))
546 (nat-less-than count (byte-to-nat (byte 6)))))))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.