~/bend-docscommunity

proofs/math/random/proof_draws.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/random/proof_draws.bend as Proof_draws

8 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../src/math/u64.bend as W
import ../../../src/math/w64.bend as X
import ../../../spec/math/random.bend as SRM
import ./uint64n.bend as UN
import ./bounded.bend as BD
import ./wrappers.bend as WR

Templates

template Uint64n.value source · line 19 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.Uint64n.value(S, next, s, n)

template Uint64n.lt source · line 22 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(n) == False{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.Uint64n.lt(S, next, s, n, hn)

template Uint32.value source · line 25 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.Uint32.value(S, next, s)

template Int64.value source · line 28 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.Int64.value(S, next, s)

template Int32.value source · line 31 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.Int32.value(S, next, s)

template Uint32n.lt source · line 34 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> @+n:U32 -> @+hn:{U32.is_zero(n) == False{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.Uint32n.lt(S, next, s, n, hn)

template Intn.lt source · line 37 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> @+n:Nat -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> @+hw:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, n) == True{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.Intn.lt(S, next, s, n, hn, hw)

template IntRange.bounds source · line 40 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> @+lo:Nat -> @+hi:Nat -> @+h:{Nat.is_lt(lo, hi) == True{} : Bool} -> @+hw:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, Nat.sub(hi, lo)) == True{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.IntRange.bounds(S, next, s, lo, hi, h, hw)