# mathlibdocumentation

core.system.random

@[class]
structure random_gen  :
Type uType u
• range : g →
• next : g → × g
• split : g → g × g

Instances
structure std_gen  :
Type

def std_range  :

Equations
@[instance]

Equations
def std_next  :

Equations
def std_split  :

Equations
@[instance]

Equations
def mk_std_gen  :
( := 0)std_gen

Return a standard number generator.

Equations
• = let q : := 0 := s / 2147483562, s1 : := 0 := s % 2147483562, s2 : := 0 := q % 2147483398 in {s1 := s1 + 1, s2 := s2 + 1}
def rand_nat {gen : Type u} [random_gen gen] :
gen → × gen

Generate a random natural number in the interval [lo, hi].

Equations
• lo hi = let lo' : := ite (lo > hi) hi lo, hi' : := ite (lo > hi) lo hi in rand_nat._match_2 g lo' hi'
• rand_nat._match_2 g lo' hi' (gen_lo, gen_hi) = let gen_mag : := gen_hi - gen_lo + 1, q : := 1000, k : := hi' - lo' + 1, tgt_mag : := k * q in rand_nat._match_1 lo' k (rand_nat_aux gen_lo gen_mag _ tgt_mag 0 g)
• rand_nat._match_1 lo' k (v, g') = let v' : := lo' + v % k in (v', g')
def rand_bool {gen : Type u} [random_gen gen] :
gen → bool × gen

Generate a random Boolean.

Equations
• = rand_bool._match_1 (rand_nat g 0 1)
• rand_bool._match_1 (v, g') = (to_bool (v = 1) 1), g')