def w8s_to_app

bend-osdev-bytes@0.1.1.0 · PROOF.bend:175

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

175def w8s_to_app(xs: List<&2, B.OctByte>, ys: List<&2, B.OctByte>) -> {B.w8s.to_list(List.append(&2, B.OctByte, xs, ys)) == B.append(B.w8s.to_list(xs), B.w8s.to_list(ys)) : List<&2, U32>}:
176  match xs:
177    case Nil{}:
178      {==}
179    case Con{h, t}:
180      %w8s_to_app(t, ys) : {Con{B.oct.to(h), B.w8s.to_list(List.append(&2, B.OctByte, t, ys))} == Con{B.oct.to(h), _} : List<&2, U32>}
181      {==}