law split_short

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

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

122# fewer than 16 bytes are all tail
123law split_short:
124  for ys: List<&2, U32>
125  for h1: {Nat.is_lt(B.len(ys), 16n) == True{} : Bool}
126  {M.cm.split(ys) == M.CmSplit{Nil{}, ys} : M.CmSplit}