law octets_of_list_idempotent

bend-osdev-bytes@0.1.1.0 · LAWS.bend:100

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

100# of_list masks once: converting a byte string to a list and back changes nothing
101law octets_of_list_idempotent:
102  for xs: List<&2, U32>
103  {B.Octets.of_list(B.Octets.to_list(B.Octets.of_list(xs))) == B.Octets.of_list(xs) : B.Octets}

Uses (6)

Used by (4)