law find_some

bend-osdev-algo@0.1.0.0 · LAWS.bend:248

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

248law find_some:
249  for xs: List<&2, U32>
250  for key: U32
251  for i: Nat
252  for e: {S.bsearch.find(xs, key) == Some{i} : Maybe<&2, Nat>}
253  {List.get(&2, U32, xs, i) == Some{key} : Maybe<&2, U32>}