def bs.find_some

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

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

1212def bs.find_some(+xs: List<&2, U32>, +key: U32, +i: Nat, e: {S.bsearch.find(xs, key) == Some{i} : Maybe<&2, Nat>}) -> {List.get(&2, U32, xs, i) == Some{key} : Maybe<&2, U32>}:
1213  bs.some(List.get(&2, U32, xs, S.bsearch.lower_bound(xs, key)), key, xs, S.bsearch.lower_bound(xs, key), i, {==}, e)