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

class RandomGen (g : Type u) :
  • 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).

Interface for random number generators.

    structure StdGen :

    "Standard" random number generator.

    Instances For
      Instances For
        Instances For
          Instances For

            Return a standard number generator.

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

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

                Generate a random Boolean.

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