law vec_lower_bound

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

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

351law vec_lower_bound:
352  {(S.bsearch.lower_bound([1, 3, 3, 7, 9], 3), S.bsearch.lower_bound([1, 3, 3, 7, 9], 10), S.bsearch.find([1, 3, 3, 7, 9], 7), S.bsearch.find([1, 3, 3, 7, 9], 8)) == (1n, 5n, Some{3n}, None{}) : Nat & Nat & Maybe<&2, Nat> & Maybe<&2, Nat>}