def hit_acc
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/lemire.bend as Lemireimport Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as SR
47# the hit of an accepted or rejected hi
48def hit_acc(+hi: Nat, +k: Nat, +ok: Bool) -> Nat:
49 SR.hit(SR.accept(hi, ok), k)
Uses (4)
Used by (7)
- bend-collections-laws-crypto@1.0.0.0/proofs/math/random/lemire:fin_eq
- bend-collections-laws-crypto@1.0.0.0/proofs/math/random/lemire:fin_gt
- bend-collections-laws-crypto@1.0.0.0/proofs/math/random/lemire:fin_lt
- bend-collections-laws-crypto@1.0.0.0/proofs/math/random/lemire:term_cases
- bend-collections-laws-crypto@1.0.0.0/proofs/math/random/lemire:term_eq
- …