def bs.check_shift

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

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

1163def bs.check_shift(m: Maybe<&2, U32>, +i: Nat, +key: U32, e: {S.bsearch.find.check(1n+i, m, key) == None{} : Maybe<&2, Nat>}) -> {S.bsearch.find.check(i, m, key) == None{} : Maybe<&2, Nat>}:
1164  match m:
1165    case None{}:
1166      {==}
1167    case Some{y}:
1168      bs.hit_shift(U32.is_eq(y, key), i, e)