`input` begins with `prefix`
461def aosHasPrefix =
462 (lambda unrestricted prefix : Bytes .
463 (lambda unrestricted input : Bytes .
464 (app
465 (bytes-eliminate
466 (lambda unrestricted current : Bytes . (pi unrestricted rest : Bytes . Nat))
467 (lambda unrestricted rest : Bytes . 1)
468 (lambda unrestricted head : Byte .
469 (lambda unrestricted tail : Bytes .
470 (lambda unrestricted induction : (pi unrestricted rest : Bytes . Nat) .
471 (lambda unrestricted rest : Bytes .
472 (naturalAnd
473 (naturalNonzero (bytes-length rest))
474 (naturalAnd (byte-equal head (bytes-head rest)) (induction (bytes-tail rest))))))))
475 prefix)
476 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.