Documentation

Init.Data.Random

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.

Instances
    structure StdGen :

    "Standard" random number generator.

    Instances For
      Equations
      Equations
      Instances For
        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.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations

            Return a standard number generator.

            Equations
            • mkStdGen s = 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.rand (lo : Nat) (hi : Nat) :
                  Equations
                  Instances For