def Uint32n.lt

bend-collections-laws-crypto@1.0.0.0 · spec/math/random.bend:143

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
import bend-collections-laws-crypto@1.0.0.0/src/math/random/rand.bend as R

143def Uint32n.lt(~S: Data, ~next: S -> W.U64 & S, +s: S, +n: U32, +hn: {U32.is_zero(n) == False{} : Bool}) -> Type:
144  {Nat.is_lt(U32.to_nat(R.fst(U32, S, R.uint32n(~S, ~next, s, n))), U32.to_nat(n)) == True{} : Bool}