def p_at_take

bend-osdev-bytes@0.1.1.0 · PROOF.bend:1264

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

1264def p_at_take(+n: Nat, +o: B.Octets, +i: Nat, h: {Nat.is_lt(i, n) == True{} : Bool}) -> {B.Octets.at(B.Octets.take(n, o), i) == B.Octets.at(o, i) : Maybe<&2, U32>}:
1265  match o:
1266    case B.Octets{+ws}:
1267      %F_take(n, ws) : {B.w8s.at(B.w8s.drop(i, _)) == B.w8s.at(B.w8s.drop(i, ws)) : Maybe<&2, U32>}
1268      off.at_take(i, n, ws, h)