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 #

@[reducible, 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
Instances For

    Lift Random.random to the Gen monad.

    Equations
    Instances For
      def SlimCheck.Gen.choose (α : Type u) [Preorder α] [BoundedRandom Id α] (lo : α) (hi : α) (h : lo hi) :
      SlimCheck.Gen { a : α // lo a a hi }

      Lift BoundedRandom.randomR to the Gen monad.

      Equations
      Instances For
        theorem SlimCheck.Gen.chooseNatLt_aux {lo : } {hi : } (a : ) (h : lo.succ a a hi) :
        lo a.pred a.pred < 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
        Instances For

          Get access to the size parameter of the Gen monad.

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

            Apply a function to the size parameter.

            Equations
            Instances For

              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.
              Instances For

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

                Equations
                • x.listOf = x.arrayOf >>= pure Array.toList
                Instances For
                  def SlimCheck.Gen.oneOf {α : Type u} (xs : Array (SlimCheck.Gen α)) (pos : autoParam (0 < xs.size) _auto✝) :

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

                  Equations
                  Instances For
                    def SlimCheck.Gen.elements {α : Type u} (xs : List α) (pos : 0 < xs.length) :

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

                    Equations
                    Instances For
                      def SlimCheck.Gen.permutationOf {α : Type u} (xs : List α) :
                      SlimCheck.Gen { ys : List α // xs.Perm ys }

                      Generate a random permutation of a given list.

                      Equations
                      Instances For
                        def SlimCheck.Gen.prodOf {α : Type u} {β : Type v} (x : SlimCheck.Gen α) (y : SlimCheck.Gen β) :

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

                        Equations
                        • x.prodOf y = do let __discrULiftable.up x match __discr with | { down := a } => do let __discrULiftable.up y match __discr with | { down := b } => pure (a, b)
                        Instances For
                          def SlimCheck.Gen.run {α : Type} (x : SlimCheck.Gen α) (size : ) :

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

                          Equations
                          Instances For