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 : gNat × Nat

    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

      The range of values returned by StdGen

      Equations
        Instances For
          Equations

            The next value from a StdGen, paired with an updated generator state.

            Equations
              Instances For

                Splits a StdGen into two separate states.

                Equations
                  Instances For
                    def mkStdGen (s : Nat := 0) :

                    Returns a standard number generator.

                    Equations
                      Instances For
                        def randNat {gen : Type u} [RandomGen gen] (g : gen) (lo hi : Nat) :
                        Nat × gen

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

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

                            Generates a random Boolean.

                            Equations
                              Instances For

                                Seeds the random number generator state used by IO.rand.

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

                                    Returns a pseudorandom number between lo and hi, using and updating a saved random generator state.

                                    This state can be seeded using IO.setRandSeed.

                                    Equations
                                      Instances For