~/bend-docscommunity

proofs/math/random/bounded.bend checks

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

11 imports
import Base
import ../../../src/math/u64.bend as W
import ../../../src/math/w64.bend as X
import ../../../src/math/random/rand.bend as R
import ../../../spec/math/w64.bend as SW
import ../../../spec/math/random.bend as SRM
import ../../../spec/math/random/rand.bend as SR
import ../../lib/logic.bend as L
import ../typed/w64add.bend as WA
import ./uint64n.bend as UN
import ./below.bend as BL

Definitions

def fst_val source · line 16 · raw

@-S:Data -> @r:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/random/below.pfst(S, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.val_pair(S, r)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.fst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S, r)) : Nat}

def nz_pos source · line 21 · raw

@+v:Nat -> @+h:{Nat.is_eq(v, 0n) == False{} : Bool} -> {Nat.is_lt(0n, v) == True{} : Bool}

Templates

template uint64n_lt source · line 28 · 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)