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 #

Tags #

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 : Random α] :

Lift Random.random to the Gen monad.

Equations
def SlimCheck.Gen.choose (α : Type u) [inst : Preorder α] [inst : BoundedRandom α] (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) :
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 : SlimCheck.Gen α) :

Apply a function to the size parameter.

Equations

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.

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

Equations

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 < List.length xs) :

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
def SlimCheck.Gen.prodOf {α : Type u} {β : Type u} (x : SlimCheck.Gen α) (y : SlimCheck.Gen β) :

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

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

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

Equations