mathlib documentation

core / system.random

@[class]
structure random_gen (g : Type u) :
Type u
Instances
structure std_gen  :
Type
def std_range  :
Equations
@[protected, instance]
Equations
def std_next  :
Equations
Equations
@[protected, instance]
Equations
def mk_std_gen (s : := 0) :

Return a standard number generator.

Equations
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
  • rand_nat g lo hi = let lo' : := ite (lo > hi) hi lo, hi' : := ite (lo > hi) lo hi in rand_nat._match_2 g lo' hi' (random_gen.range g)
  • 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