law split_bytes_onto

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

import Base
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M

74# splitting the bytes of a block gives the block back
75law split_bytes_onto:
76  for b: M.CmBlock
77  for rest: List<&2, U32>
78  {M.cm.split(M.cm.bytes_onto(b, rest)) == M.cm.split.cons(b, M.cm.split(rest)) : M.CmSplit}