Documentation

Mathlib.Control.Random

Rand Monad and Random Class #

This module provides tools for formulating computations guided by randomness and for defining objects that can be created randomly.

Main definitions #

References #

@[inline, reducible]
abbrev RandG (g : Type) (α : Type u_1) :
Type u_1

A monad to generate random objects using the generic generator type g

Instances For
    @[inline, reducible]
    abbrev Rand (α : Type u) :

    A monad to generate random objects using the generator type Rng

    Instances For
      class Random (α : Type u) :
      Type (max 1 u)

      Random α gives us machinery to generate values of type α

      Instances
        class BoundedRandom (α : Type u) [Preorder α] :
        Type (max 1 u)

        BoundedRandom α gives us machinery to generate values of type α between certain bounds

        Instances
          def Rand.next {g : Type} [RandomGen g] :

          Generate one more Nat

          Instances For
            def Rand.split {g : Type} [RandomGen g] :
            RandG g g

            Create a new random number generator distinct from the one stored in the state

            Instances For
              def Rand.range {g : Type} [RandomGen g] :

              Get the range of Nat that can be generated by the generator g

              Instances For
                def Random.rand {g : Type} (α : Type u) [Random α] [RandomGen g] :
                RandG g α

                Generate a random value of type α.

                Instances For
                  def Random.randBound {g : Type} (α : Type u) [Preorder α] [BoundedRandom α] (lo : α) (hi : α) (h : lo hi) [RandomGen g] :
                  RandG g { a // lo a a hi }

                  Generate a random value of type α between x and y inclusive.

                  Instances For
                    def Random.randFin {g : Type} {n : } [RandomGen g] :
                    Instances For
                      Instances For
                        def IO.runRand {α : Type} (cmd : Rand α) :

                        Computes a Rand α using the global stdGenRef as RNG. Note that:

                        • stdGenRef is not necessarily properly seeded on program startup as of now and will therefore be deterministic.
                        • stdGenRef is not thread local, hence two threads accessing it at the same time will get the exact same generator.
                        Instances For
                          def IO.runRandWith {α : Type} (seed : ) (cmd : Rand α) :
                          Instances For