Documentation

Plausible.Gen

Gen Monad #

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

Main definitions #

References #

@[reducible, inline]
abbrev Plausible.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
      @[inline]
      def Plausible.Gen.up {α : Type u} (x : Gen α) :
      Gen (ULift α)
      Equations
        Instances For
          @[inline]
          def Plausible.Gen.down {α : Type u_1} (x : Gen (ULift α)) :
          Gen α
          Equations
            Instances For
              def Plausible.Gen.chooseAny (α : Type u) [Random Id α] :
              Gen α

              Lift Random.random to the Gen monad.

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

                  Lift BoundedRandom.randomR to the Gen monad.

                  Equations
                    Instances For
                      def Plausible.Gen.chooseNatLt (lo hi : Nat) (h : lo < hi) :
                      Gen { a : Nat // lo a a < hi }

                      Generate a Nat example between lo and hi (exclusively).

                      Equations
                        Instances For

                          Get access to the size parameter of the Gen monad.

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

                              Apply a function to the size parameter.

                              Equations
                                Instances For

                                  Choose a Nat between 0 and getSize.

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

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

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

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

                                          Equations
                                            Instances For
                                              def Plausible.Gen.oneOf {α : Type u} (xs : Array (Gen α)) (pos : 0 < xs.size := by decide) :
                                              Gen α

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

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

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

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

                                                      Generate a random permutation of a given list.

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

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

                                                          Equations
                                                            Instances For
                                                              def Plausible.Gen.run {α : Type} (x : Gen α) (size : Nat) :

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

                                                              Equations
                                                                Instances For