ProofBsearch.bq.pick_eq: def of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as ProofBsearch
Lines 91-96 of bend-osdev-algo@0.1.0.0/proof_bsearch.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&start_line=91&end_line=96

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

def 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}:
  match b:
    case True{}:
      {==}
    case False{}:
      {==}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/bsearch.bend&name=BsearchState
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/bsearch.bend&name=bsearch.array.pick
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.hi_b
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.lo_b