law lower_bound_below

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

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

229law lower_bound_below:
230  for xs: List<&2, U32>
231  for key: U32
232  for i: Nat
233  for x: U32
234  for e: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
235  for l: {Nat.is_lt(i, S.bsearch.lower_bound(xs, key)) == True{} : Bool}
236  {U32.is_lt(x, key) == True{} : Bool}