law join_split

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

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

86# a masked list is its blocks and its tail joined back
87law join_split:
88  for ys: List<&2, U32>
89  {M.cm.join_onto(M.cm.split.blocks(M.cm.split(B.mask(ys))), M.cm.split.tail(M.cm.split(B.mask(ys)))) == B.mask(ys) : List<&2, U32>}