law octets_slice_take

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

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

381law octets_slice_take:
382  for +m: Nat
383  for +i: Nat
384  for +n: Nat
385  for +o: B.Octets
386  for h: {Nat.is_le(Nat.add(i, n), m) == True{} : Bool}
387  {B.Octets.slice(i, n, B.Octets.take(m, o)) == B.Octets.slice(i, n, o) : B.Octets}