95def aosAllBytes =
96 (lambda unrestricted predicate : (pi unrestricted b : Byte . Nat) . (lambda unrestricted input : Bytes .
97 (bytes-eliminate (lambda unrestricted current : Bytes . Nat) 1
98 (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : Nat .
99 (naturalAnd (predicate head) induction))))
100 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.