def bq.step_eq

bend-osdev-algo@0.1.0.0 · proof_bsearch.bend:98

import Base
import bend-osdev-algo@0.1.0.0/bsearch.bend as S

98def bq.step_eq(c: Bool, -a: Array<U32>, +x: U32, +key: U32, +lo: U32, +hi: U32, +mid: U32) -> {S.bsearch.array.step(c, (a, x), key, lo, hi, mid) == S.BsearchState{a, bq.nlo.a(c, U32.is_lt(x, key), lo, mid), bq.nhi.a(c, U32.is_lt(x, key), hi, mid)} : S.BsearchState}:
99  match c:
100    case True{}:
101      bq.pick_eq(U32.is_lt(x, key), a, lo, hi, mid)
102    case False{}:
103      {==}