def w8s_len

bend-osdev-bytes@0.1.1.1 · PROOF.bend:183

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

183def w8s_len(ws: List<&2, B.OctByte>) -> {List.length(&2, B.OctByte, ws) == List.length(&2, U32, B.w8s.to_list(ws)) : Nat}:
184  match ws:
185    case Nil{}:
186      {==}
187    case Con{h, t}:
188      Equal.cong(Nat, Nat, k => 1n+k, List.length(&2, B.OctByte, t), List.length(&2, U32, B.w8s.to_list(t)), w8s_len(t))