def p_take_len

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

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

1337def p_take_len(+o: B.Octets) -> {B.Octets.take(B.Octets.len(o), o) == o : B.Octets}:
1338  match o:
1339    case B.Octets{+ws}:
1340      %F_take(B.w8s.len.fast(ws), ws) : {B.Octets{_} == B.Octets{ws} : B.Octets}
1341      %F_len(ws) : {B.Octets{B.w8s.take(_, ws)} == B.Octets{ws} : B.Octets}
1342      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.take(List.length(&2, B.OctByte, ws), ws), ws, off.take_len(ws))