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

class RandomGen (g : Type u) : Type u

• range : g → Nat × Nat

  range returns the range of values returned by the generator.

• next : g → Nat × 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 : g → g × 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).

Interface for random number generators.

structure StdGen : Type

• s1 : Nat
• s2 : Nat

"Standard" random number generator.

instance instInhabitedStdGen : Inhabited StdGen

def stdRange : Nat × Nat

instance instReprStdGen : Repr StdGen

def stdNext : StdGen → Nat × StdGen

def stdSplit : StdGen → StdGen × StdGen

instance instRandomGenStdGen : RandomGen StdGen

def mkStdGen (s : optParam Nat 0) : StdGen

Return a standard number generator.

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].

def randBool {gen : Type u} [RandomGen gen] (g : gen) : Bool × gen

Generate a random Boolean.

opaque IO.stdGenRef : IO.Ref StdGen

def IO.setRandSeed (n : Nat) : IO Unit

def IO.rand (lo : Nat) (hi : Nat) : IO Nat