These helpers are called only after a public bounds proof.
303def dataBytesDropValidated =
304 (lambda unrestricted count : Nat .
305 (nat-eliminate
306 (lambda unrestricted current : Nat . (pi unrestricted input : Bytes . Bytes))
307 (lambda unrestricted input : Bytes . input)
308 (lambda unrestricted predecessor : Nat .
309 (lambda unrestricted induction : (pi unrestricted input : Bytes . Bytes) .
310 (lambda unrestricted input : Bytes . (induction (bytes-tail input)))))
311 count))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.