def again
import bend-collections-laws-crypto@1.0.0.0/src/math/random/rand.bend as Randimport Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
119# one rejection step: while lo < t, draw again; an accepted draw is kept
120def again(~S: Data, ~next: S -> W.U64 & S, +n: W.U64, +hi: W.U64, +lo: W.U64, s: S, reject: Bool) -> Draw<S>:
121 match reject:
122 case False{}:
123 D{hi, lo, s}
124 case True{}:
125 draw(S, n, next(s))
Uses (5)
Used by (5)
- bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n:fixpoint
- bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n:step_case
- bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n:step_false
- bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n:step_true
- bend-collections-laws-crypto@1.0.0.0/src/math/random/rand:step