def p_octets_len_list

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

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

421def p_octets_len_list(+o: B.Octets) -> {B.Octets.len(o) == B.len(B.Octets.to_list(o)) : Nat}:
422  match o:
423    case B.Octets{+ws}:
424      %F_len(ws) : {_ == B.len(B.w8s.to_list.fast(ws)) : Nat}
425      %F_to(ws) : {List.length(&2, B.OctByte, ws) == B.len(_) : Nat}
426      w8s_len(ws)