law wit_bsearch

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

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

381# a sorted list; an element before the lower bound of 7 (index 1) and one
382# from it on (index 4); find answering Some and None
383law wit_bsearch:
384  {(S.bsearch.sorted([1, 3, 3, 7, 9]), S.bsearch.lower_bound([1, 3, 3, 7, 9], 7), List.get(&2, U32, [1, 3, 3, 7, 9], 1n), List.get(&2, U32, [1, 3, 3, 7, 9], 4n), S.bsearch.find([1, 3, 3, 7, 9], 7), S.bsearch.find([1, 3, 3, 7, 9], 8)) == (True{}, 3n, Some{3}, Some{9}, Some{3n}, None{}) : Bool & Nat & Maybe<&2, U32> & Maybe<&2, U32> & Maybe<&2, Nat> & Maybe<&2, Nat>}