law append_pair

lawful-bytes@0.1.1.0 · LAWS.bend:213

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

213# append hands src back (as a literal pair, for rewriting).
214law append_pair:
215  for dst: D.Bytes
216  for src: D.Bytes
217  for s: U32
218  for n: U32
219  {B.append(dst, src, s, n) == (Pair.fst(D.Bytes, D.Bytes, B.append(dst, src, s, n)), src) : D.Bytes & D.Bytes}