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 #

source
@[inline, reducible]
abbrev SlimCheck.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.

Instances For
    source
    def SlimCheck.Gen.chooseAny (α : Type u) [Random α] :
    SlimCheck.Gen α

    Lift Random.random to the Gen monad.

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

      Lift BoundedRandom.randomR to the Gen monad.

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

        Instances For
          source
          def SlimCheck.Gen.getSize :
          SlimCheck.Gen ℕ

          Get access to the size parameter of the Gen monad.

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

            Apply a function to the size parameter.

            Instances For
              source
              def SlimCheck.Gen.arrayOf {α : Type u} (x : SlimCheck.Gen α) :
              SlimCheck.Gen (Array α)

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

              Instances For
                source
                def SlimCheck.Gen.listOf {α : Type u} (x : SlimCheck.Gen α) :
                SlimCheck.Gen (List α)

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

                Instances For
                  source
                  def SlimCheck.Gen.oneOf {α : Type u} (xs : Array (SlimCheck.Gen α)) (pos : autoParam (0 < Array.size xs) _auto✝) :
                  SlimCheck.Gen α

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

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

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

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

                      Generate a random permutation of a given list.

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

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

                        Instances For
                          source
                          def SlimCheck.Gen.run {α : Type} (x : SlimCheck.Gen α) (size : ℕ) :
                          BaseIO α

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

                          Instances For