`input` without its first `count` bytes
479def aosDropBytes =
480 (lambda unrestricted count : Nat .
481 (lambda unrestricted input : Bytes .
482 (app
483 (nat-eliminate
484 (lambda unrestricted current : Nat . (pi unrestricted rest : Bytes . Bytes))
485 (lambda unrestricted rest : Bytes . rest)
486 (lambda unrestricted predecessor : Nat .
487 (lambda unrestricted induction : (pi unrestricted rest : Bytes . Bytes) .
488 (lambda unrestricted rest : Bytes . (induction (bytes-tail rest)))))
489 count)
490 input)))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.