PROOF.eq_go: def of bend-osdev-bytes@0.1.1.0
Import: import bend-osdev-bytes@0.1.1.0/PROOF.bend as PROOF
Lines 640-665 of bend-osdev-bytes@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-bytes@0.1.1.0/PROOF.bend&start_line=640&end_line=665

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

def eq_go(+xs: List<&2, U32>, +ys: List<&2, U32>, +ok: Bool) -> {B.list_eq.go(xs, ys, ok) == Bool.and(ok, B.list_eq(xs, ys)) : Bool}:
  match xs ys:
    case Nil{} Nil{}:
      match ok:
        case True{}:
          {==}
        case False{}:
          {==}
    case Con{a, s} Con{b, t}:
      match ok:
        case True{}:
          eq_go(s, t, U32.is_eq(a, b))
        case False{}:
          eq_go(s, t, False{})
    case Nil{} Con{b, t}:
      match ok:
        case True{}:
          {==}
        case False{}:
          {==}
    case Con{a, s} Nil{}:
      match ok:
        case True{}:
          {==}
        case False{}:
          {==}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=list_eq
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=list_eq.go