mathlib documentation

core.​system.​random

core.​system.​random

@[class]
structure random_gen  :
Type uType u

Instances
structure std_gen  :
Type

def std_range  :

Equations
@[instance]

Equations
def std_next  :

Equations

Equations
def mk_std_gen  :
( := 0)std_gen

Return a standard number generator.

Equations
def rand_nat {gen : Type u} [random_gen gen] :
gen → × 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] :
gen → bool × gen

Generate a random Boolean.

Equations