102def aosAnyByte =
103 (lambda unrestricted predicate : (pi unrestricted b : Byte . Nat) . (lambda unrestricted input : Bytes .
104 (bytes-eliminate (lambda unrestricted current : Bytes . Nat) 0
105 (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : Nat .
106 (naturalOr (predicate head) induction))))
107 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.