def eq_go

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

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

640def 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}:
641  match xs ys:
642    case Nil{} Nil{}:
643      match ok:
644        case True{}:
645          {==}
646        case False{}:
647          {==}
648    case Con{a, s} Con{b, t}:
649      match ok:
650        case True{}:
651          eq_go(s, t, U32.is_eq(a, b))
652        case False{}:
653          eq_go(s, t, False{})
654    case Nil{} Con{b, t}:
655      match ok:
656        case True{}:
657          {==}
658        case False{}:
659          {==}
660    case Con{a, s} Nil{}:
661      match ok:
662        case True{}:
663          {==}
664        case False{}:
665          {==}