def p_octets_zeros_list

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

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

476def p_octets_zeros_list(+n: Nat) -> {B.Octets.to_list(B.Octets.zeros(n)) == B.zeros(n) : List<&2, U32>}:
477  %F_to(B.w8s.zeros.fast(n)) : {_ == B.zeros(n) : List<&2, U32>}
478  %F_zeros(n) : {B.w8s.to_list(_) == B.zeros(n) : List<&2, U32>}
479  w8s_zeros_list(n)