# Documentation

Mathlib.Control.Random

# Rand Monad and Random Class #

This module provides tools for formulating computations guided by randomness and for defining objects that can be created randomly.

## Main definitions #

• Rand and RandG monad for computations guided by randomness;
• Random class for objects that can be generated randomly;
• random to generate one object;
• BoundedRandom class for objects that can be generated randomly inside a range;
• randomR to generate one object inside a range;
• IO.runRand to run a randomized computation inside the IO monad;

## References #

@[inline]
abbrev RandG (g : Type) (α : Type u_1) :
Type u_1

A monad to generate random objects using the generic generator type g

Equations
@[inline]
abbrev Rand (α : Type u) :

A monad to generate random objects using the generator type Rng

Equations
class Random (α : Type u) :
Type (max1u)
• random : {g : Type} → [inst : ] → RandG g α

Random α gives us machinery to generate values of type α

Instances
class BoundedRandom (α : Type u) [inst : ] :
Type (max1u)
• randomR : {g : Type} → (lo hi : α) → lo hi[inst : ] → RandG g { a // lo a a hi }

BoundedRandom α gives us machinery to generate values of type α between certain bounds

Instances
def Rand.next {g : Type} [inst : ] :

Generate one more Nat

Equations
• Rand.next = do let __do_lift ← get let rng : g := __do_lift.down match with | (res, new) => do set { down := new } pure res
def Rand.split {g : Type} [inst : ] :
RandG g g

Create a new random number generator distinct from the one stored in the state

Equations
• Rand.split = do let __do_lift ← get let rng : g := __do_lift.down match with | (r1, r2) => do set { down := r1 } pure r2
def Rand.range {g : Type} [inst : ] :
RandG g ()

Get the range of Nat that can be generated by the generator g

Equations
• Rand.range = do let __do_lift ← get let rng : g := __do_lift.down pure ()
def Random.rand {g : Type} (α : Type u) [inst : ] [inst : ] :
RandG g α

Generate a random value of type α.

Equations
• = Random.random
def Random.randBound {g : Type} (α : Type u) [inst : ] [inst : ] (lo : α) (hi : α) (h : lo hi) [inst : ] :
RandG g { a // lo a a hi }

Generate a random value of type α between x and y inclusive.

Equations
def Random.randFin {g : Type} {n : } [inst : ] :
RandG g (Fin ())
Equations
instance Random.instRandomFinSucc {n : } :
Random (Fin ())
Equations
• Random.instRandomFinSucc = { random := fun {g} [] => Random.randFin }
def Random.randBool {g : Type} [inst : ] :
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def IO.runRand {α : Type} (cmd : Rand α) :

Computes a Rand α using the global stdGenRef as RNG. Note that:

• stdGenRef is not necessarily properly seeded on program startup as of now and will therefore be deterministic.
• stdGenRef is not thread local, hence two threads accessing it at the same time will get the exact same generator.
Equations
• One or more equations did not get rendered due to their size.
def IO.runRandWith {α : Type} (seed : ) (cmd : Rand α) :
Equations