def bq.lb

bend-osdev-algo@0.1.0.0 · proof_bsearch.bend:36

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

36def bq.lb(+l: List<&2, U32>, +n: U32, +key: U32) -> Nat:
37  S.bsearch.lower_bound(List.take(&2, U32, l, U32.to_nat(n)), key)