# Documentation

Mathlib.Testing.SlimCheck.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 #

• Gen monad

random testing

## References #

@[inline]
abbrev SlimCheck.Gen (α : 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
def SlimCheck.Gen.chooseAny (α : Type u) [inst : ] :

Lift Random.random to the Gen monad.

Equations
def SlimCheck.Gen.choose (α : Type u) [inst : ] [inst : ] (lo : α) (hi : α) (h : lo hi) :
SlimCheck.Gen { a // lo a a hi }

Lift BoundedRandom.randomR to the Gen monad.

Equations
theorem SlimCheck.Gen.chooseNatLt_aux {lo : } {hi : } (a : ) (h : Nat.succ lo a a hi) :
lo < hi
def SlimCheck.Gen.chooseNatLt (lo : ) (hi : ) (h : lo < hi) :
SlimCheck.Gen { a // lo a a < hi }

Generate a Nat example between x and y (exclusively).

Equations
• One or more equations did not get rendered due to their size.

Get access to the size parameter of the Gen monad.

Equations
def SlimCheck.Gen.resize {α : Type u_1} (f : ) (x : ) :

Apply a function to the size parameter.

Equations
def SlimCheck.Gen.arrayOf {α : Type} (x : ) :

Create an Array of examples using x. The size is controlled by the size parameter of Gen.

Equations
• One or more equations did not get rendered due to their size.
def SlimCheck.Gen.listOf {α : Type} (x : ) :

Create an List of examples using x. The size is controlled by the size parameter of Gen.

Equations
def SlimCheck.Gen.oneOf {α : Type} (xs : ) (pos : autoParam (0 < ) _auto✝) :

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

Equations
• One or more equations did not get rendered due to their size.
def SlimCheck.Gen.elements {α : Type} (xs : List α) (pos : 0 < ) :

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

Equations
• One or more equations did not get rendered due to their size.
def SlimCheck.Gen.permutationOf {α : Type} (xs : List α) :
SlimCheck.Gen { ys // ys ~ xs }

Generate a random permutation of a given list.

Equations
• One or more equations did not get rendered due to their size.
• = pure { val := [], property := (_ : [] ~ []) }
def SlimCheck.Gen.prodOf {α : Type u} {β : Type u} (x : ) (y : ) :

Given two generators produces a tuple consisting out of the result of both

Equations
• = do let __do_lift ← x let __do_lift_1 ← y pure (__do_lift, __do_lift_1)
def SlimCheck.Gen.run {α : Type} (x : ) (size : ) :

Execute a Gen inside the IO monad using size as the example size

Equations