def bq.pick_eq

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

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

91def bq.pick_eq(b: Bool, -a: Array<U32>, +lo: U32, +hi: U32, +mid: U32) -> {S.bsearch.array.pick(b, a, lo, hi, mid) == S.BsearchState{a, bq.lo_b(b, lo, mid), bq.hi_b(b, hi, mid)} : S.BsearchState}:
92  match b:
93    case True{}:
94      {==}
95    case False{}:
96      {==}