def p_hex_fast

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

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

633def p_hex_fast(+xs: List<&2, U32>) -> {B.hex(xs) == B.hex.fast(xs) : String}:
634  Equal.sym(String, B.hex.fast(xs), B.hex(xs),
635    Equal.trans(String, B.hex.go(B.rev_onto(xs, Nil{}), SNil{}), B.hex.cat(xs, SNil{}), B.hex(xs), h_go(xs, Nil{}, SNil{}), h_cat(xs)))