# Documentation

## Init.Data.Random

Basic random number generator support based on the one available on the Haskell library

class RandomGen (g : Type u) :

Interface for random number generators.

• range : g

range returns the range of values returned by the generator.

• next : gNat × g

next operation returns a natural number that is uniformly distributed the range returned by range (including both end points), and a new generator.

• split : gg × g

The 'split' operation allows one to obtain two distinct random number generators. This is very useful in functional programs (for example, when passing a random number generator down to recursive calls).

Instances
structure StdGen :

"Standard" random number generator.

Instances For
Equations
def stdRange :
Equations
Instances For
instance instReprStdGen :
Equations
• One or more equations did not get rendered due to their size.
def stdNext :
Equations
• One or more equations did not get rendered due to their size.
Instances For
def stdSplit :
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
def mkStdGen (s : ) :

Return a standard number generator.

Equations
• = let q := s / 2147483562; let s1 := s % 2147483562; let s2 := q % 2147483398; { s1 := s1 + 1, s2 := s2 + 1 }
Instances For
def randNat {gen : Type u} [RandomGen gen] (g : gen) (lo : Nat) (hi : Nat) :
Nat × gen

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def randBool {gen : Type u} [RandomGen gen] (g : gen) :
Bool × gen

Generate a random Boolean.

Equations
Instances For
def IO.setRandSeed (n : Nat) :
Equations
Instances For
def IO.rand (lo : Nat) (hi : Nat) :
Equations
Instances For