~/jendhub

def bs.step0

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

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

1097def bs.step0(c: Bool, +r: Nat, l: {Nat.is_lt(0n, S.bsearch.below.step(c, r)) == True{} : Bool}) -> {c == True{} : Bool}:
1098  match c:
1099    case True{}:
1100      {==}
1101    case False{}:
1102      Empty.absurd({False{} == True{} : Bool}, absurd.ft(l))

Uses (6)

Used by (1)