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]
abbrev RandG (g : Type) (α : Type u_1) :
Type u_1

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

Equations
@[inline]
abbrev Rand (α : Type u) :

A monad to generate random objects using the generator type Rng

Equations
class Random (α : Type u) :
Type (max1u)

Random α gives us machinery to generate values of type α

Instances
    class BoundedRandom (α : Type u) [inst : Preorder α] :
    Type (max1u)

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

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

      Generate one more Nat

      Equations
      • Rand.next = do let __do_lift ← get let rng : g := __do_lift.down match RandomGen.next rng with | (res, new) => do set { down := new } pure res
      def Rand.split {g : Type} [inst : RandomGen g] :
      RandG g g

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

      Equations
      • Rand.split = do let __do_lift ← get let rng : g := __do_lift.down match RandomGen.split rng with | (r1, r2) => do set { down := r1 } pure r2
      def Rand.range {g : Type} [inst : RandomGen g] :

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

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

      Generate a random value of type α.

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

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

      Equations
      def Random.randFin {g : Type} {n : } [inst : RandomGen g] :
      Equations
      Equations
      • Random.instRandomFinSucc = { random := fun {g} [RandomGen g] => Random.randFin }
      def Random.randBool {g : Type} [inst : RandomGen g] :
      Equations
      Equations
      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.
      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.
      Equations
      • One or more equations did not get rendered due to their size.
      def IO.runRandWith {α : Type} (seed : ) (cmd : Rand α) :
      Equations