def bs.sorted_tail

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

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

1062def bs.sorted_tail(t: List<&2, U32>, x0: U32, s: {S.bsearch.sorted.pair(t, x0) == True{} : Bool}) -> {S.bsearch.sorted(t) == True{} : Bool}:
1063  match t:
1064    case Nil{}:
1065      {==}
1066    case Con{y, tt}:
1067      bool.and_r(U32.is_le(x0, y), S.bsearch.sorted.pair(tt, y), s)