def list_eq_self

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

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

382def list_eq_self(xs: List<&2, U32>) -> {B.list_eq(xs, xs) == True{} : Bool}:
383  match xs:
384    case Nil{}:
385      {==}
386    case Con{+h, +t}:
387      %Equal.sym(Bool, U32.is_eq(h, h), True{}, u32_eq_self(h)) : {Bool.and(_, B.list_eq(t, t)) == True{} : Bool}
388      list_eq_self(t)