def acc_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/below.bend:89

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as SR

89def acc_lt(+h: Nat, +k: Nat, +n: Nat, +hh: {Nat.is_lt(h, n) == True{} : Bool}, +ok: Bool, +e: {SR.accept(h, ok) == Some{k} : Maybe<&2, Nat>}) -> {Nat.is_lt(k, n) == True{} : Bool}:
90  match ok:
91    case True{}:
92      %some_inj(h, k, e) : {Nat.is_lt(_, n) == True{} : Bool}
93      hh
94    case False{}:
95      Empty.absurd({Nat.is_lt(k, n) == True{} : Bool}, none_some(k, e))