def append.go

lawful-bytes@0.1.1.0 · bytes.bend:42

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

42# n more bytes of src, from s; r holds src's byte s.
43def append.go(n: Nat, dst: D.Bytes, r: D.Bytes & U32, +s: U32) -> D.Bytes & D.Bytes:
44  match n:
45    case 0n:
46      (src, x) = r
47      (dst, src)
48    case 1n+k:
49      (src, +x) = r
50      append.go(k, push(dst, x), at(src, (s + 1 : U32)), (s + 1 : U32))