def p_len_of_list

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

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

1123def p_len_of_list(+xs: List<&2, U32>) -> {B.Octets.len(B.Octets.of_list(xs)) == B.len(xs) : Nat}:
1124  %F_of(xs) : {B.w8s.len.fast(_) == B.len(xs) : Nat}
1125  %F_len(B.w8s.of_list(xs)) : {_ == B.len(xs) : Nat}
1126  off.len_of(xs)