def bs.hit_none

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

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

1149def bs.hit_none(c: Bool, +i: Nat, e: {S.bsearch.find.hit(c, i) == None{} : Maybe<&2, Nat>}) -> {c == False{} : Bool}:
1150  match c:
1151    case True{}:
1152      Empty.absurd({True{} == False{} : Bool}, absurd.sn(i, e))
1153    case False{}:
1154      {==}