def w8s_eq_self

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

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

390def w8s_eq_self(ws: List<&2, B.OctByte>) -> {B.w8s.eq(ws, ws, True{}) == True{} : Bool}:
391  match ws:
392    case Nil{}:
393      {==}
394    case Con{+h, +t}:
395      %Equal.sym(Bool, U32.is_eq(B.oct.to(h), B.oct.to(h)), True{}, u32_eq_self(B.oct.to(h))) : {B.w8s.eq(t, t, Bool.and(True{}, _)) == True{} : Bool}
396      w8s_eq_self(t)