law fast_append_pair

lawful-bytes@0.1.1.0 · LAWS.bend:485

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/fast.bend as FA

485law fast_append_pair:
486  for dst: D.Bytes
487  for src: D.Bytes
488  for s: U32
489  for n: U32
490  {FA.append(dst, src, s, n) == (Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n)), src) : D.Bytes & D.Bytes}