def h_cat

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

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

626def h_cat(+xs: List<&2, U32>) -> {B.hex.cat(xs, SNil{}) == B.hex(xs) : String}:
627  match xs:
628    case Nil{}:
629      {==}
630    case Con{h, t}:
631      Equal.cong(String, String, x => SCon{B.hex.digit(U32.shrn(B.byte(h), 4n)), SCon{B.hex.digit(U32.and(B.byte(h), 15)), x}}, B.hex.cat(t, SNil{}), B.hex(t), h_cat(t))