mathlib documentation

testing.slim_check.gen

gen Monad

This monad is used to formulate randomized computations with a parameter to specify the desired size of the result.

This is a port of the Haskell QuickCheck library.

Main definitions

Local notation

Tags

random testing

References

source
@[instance]
def slim_check.gen.monad  :
monad slim_check.gen

source
def slim_check.gen (α : Type u) :
Type u

Monad to generate random examples to test properties with. It has a nat parameter so that the caller can decide on the size of the examples.

Equations
source
@[instance]
def slim_check.gen.is_lawful_monad  :
is_lawful_monad slim_check.gen

source
def slim_check.io.run_gen {α : Type} (x : slim_check.gen α) (i : ℕ) :
io α

Execute a gen inside the io monad using i as the example size and with a fresh random number generator.

Equations
source
def slim_check.gen.choose_any (α : Type u) [preorder α] [random α] :
slim_check.gen α

Lift random.random to the gen monad.

Equations
source
def slim_check.gen.choose {α : Type u} [preorder α] [bounded_random α] (x y : α) (p : x ≤ y) :
slim_check.gen ↥(set.Icc x y)

Lift random.random_r to the gen monad.

Equations
source
def slim_check.gen.choose_nat (x y : ℕ) (p : x ≤ y) :
slim_check.gen ↥(set.Icc x y)

Generate a nat example between x and y.

Equations
source
@[instance]
def slim_check.gen.uliftable  :
uliftable slim_check.gen slim_check.gen

Equations
source
@[instance]
def slim_check.gen.has_orelse  :
has_orelse slim_check.gen

Equations
source
def slim_check.gen.sized {α : Type u} (cmd : ℕ → slim_check.gen α) :
slim_check.gen α

Get access to the size parameter of the gen monad. For reasons of universe polymorphism, it is specified in continuation passing style.

Equations
source
def slim_check.gen.vector_of {α : Type u} (n : ℕ) (cmd : slim_check.gen α) :
slim_check.gen (vector α n)

Create n examples using cmd.

Equations
source
def slim_check.gen.list_of {α : Type u} (cmd : slim_check.gen α) :
slim_check.gen (list α)

Create a list of examples using cmd. The size is controlled by the size parameter of gen.

Equations
source
def slim_check.gen.one_of_aux {α : Type u} (xs : list (slim_check.gen α)) (pos : fact (0 < xs.length)) :
slim_check.gen α

Given a list of example generators, choose one to create an example. This definition is needed for to provide a local fact $ 0 < xs.length instance to the type resolution system.

Equations
source
def slim_check.gen.one_of {α : Type u} (xs : list (slim_check.gen α)) (pos : 0 < xs.length) :
slim_check.gen α

Given a list of example generators, choose one to create an example.

Equations
source
def slim_check.gen.permutation_of {α : Type u} (xs : list α) :
slim_check.gen (subtype xs.perm)

Generate a random permutation of a given list.

Equations