def ba.fs

bend-osdev-algo@0.1.0.0 · PROOF.bend:1421

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

1421def ba.fs(c: Bool, -a0: Array<U32>, -x: U32, +r: U32, +key: U32) -> {Pair.fst(Array<U32>, Maybe<&2, U32>, S.bsearch.array.found(c, (a0, x), r, key)) == a0 : Array<U32>}:
1422  match c:
1423    case True{}:
1424      {==}
1425    case False{}:
1426      {==}