def bs.hit_shift

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

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

1156def bs.hit_shift(c: Bool, +i: Nat, e: {S.bsearch.find.hit(c, 1n+i) == None{} : Maybe<&2, Nat>}) -> {S.bsearch.find.hit(c, i) == None{} : Maybe<&2, Nat>}:
1157  match c:
1158    case True{}:
1159      Empty.absurd({Some{i} == None{} : Maybe<&2, Nat>}, absurd.sn(1n+i, e))
1160    case False{}:
1161      {==}