~/jendhub

def bs.step1

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

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

1104def bs.step1(c: Bool, +r: Nat, +i: Nat, l: {Nat.is_lt(1n+i, S.bsearch.below.step(c, r)) == True{} : Bool}) -> {Nat.is_lt(i, r) == True{} : Bool}:
1105  match c:
1106    case True{}:
1107      l
1108    case False{}:
1109      Empty.absurd({Nat.is_lt(i, r) == True{} : Bool}, absurd.ft(l))

Uses (6)

Used by (1)