def t_cat

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

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

605def t_cat(+xs: List<&2, U32>) -> {B.to_string.cat(xs, SNil{}) == B.to_string(xs) : String}:
606  match xs:
607    case Nil{}:
608      {==}
609    case Con{h, t}:
610      Equal.cong(String, String, x => SCon{Chr{B.byte(h)}, x}, B.to_string.cat(t, SNil{}), B.to_string(t), t_cat(t))