# mathlibdocumentation

core / system.random

@[class]
structure random_gen (g : Type u) :
Type u
• range : g →
• next : g → × g
• split : g → g × g
Instances of this typeclass
Instances of other typeclasses for random_gen
• random_gen.has_sizeof_inst
structure std_gen  :
Type
Instances for std_gen
def std_range  :
Equations
@[protected, instance]
Equations
def std_next  :
Equations
def std_split  :
Equations
@[protected, instance]
Equations
def mk_std_gen (s : := 0) :

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] (g : gen) (lo hi : ) :
× 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] (g : gen) :
bool × gen

Generate a random Boolean.

Equations