law octets_len_slice

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

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

260law octets_len_slice:
261  for +i: Nat
262  for +n: Nat
263  for +o: B.Octets
264  {B.Octets.len(B.Octets.slice(i, n, o)) == Nat.min(n, Nat.sub(B.Octets.len(o), i)) : Nat}