law cut_pair

lawful-fields@0.1.1.0 · LAWS.bend:53

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-fields@0.1.1.0/fields.bend as C

53law cut_pair:
54  for b: D.Bytes
55  for from: U32
56  for to: U32
57  for sep: U32
58  for n: Nat
59  {C.cut(b, from, to, sep, n) == (b, Pair.snd(D.Bytes, List<&2, U32>, C.cut(b, from, to, sep, n))) : D.Bytes & List<&2, U32>}