law octets_len

bend-osdev-mode-core@0.1.0.0 · LAWS.bend:138

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

138law octets_len:
139  for +o: B.Octets
140  for +n: Nat
141  for h: {B.Octets.len(o) == n : Nat}
142  {B.len(B.Octets.to_list(o)) == n : Nat}