def bs.le_len

bend-osdev-algo@0.1.0.0 · PROOF.bend:1090

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

1090def bs.le_len(xs: List<&2, U32>, +key: U32) -> {Nat.is_le(S.bsearch.lower_bound(xs, key), List.length(&2, U32, xs)) == True{} : Bool}:
1091  match xs:
1092    case Nil{}:
1093      {==}
1094    case Con{x, +t}:
1095      bs.le_len.h(U32.is_lt(x, key), S.bsearch.lower_bound(t, key), List.length(&2, U32, t), bs.le_len(t, key))