class Plausible.ArbitraryFueled (α : Type) : Type

A typeclass for fueled random generation, i.e. a variant of the Arbitrary typeclass where the fuel for the generator is made explicit.

• This typeclass is equivalent to Rocq QuickChick's arbitrarySized typeclass (QuickChick uses the Nat parameter as both fuel and the generator size, here we use it just for fuel, as Plausible's Gen type constructor already internalizes the size parameter.)

• arbitraryFueled : Nat → Gen α

  Takes a Nat and produces a random generator dependent on the Nat parameter (which indicates the amount of fuel to be used before failing).

instance Plausible.instArbitraryOfArbitraryFueled {α : Type} [ArbitraryFueled α] : Arbitrary α

Every ArbitraryFueled instance gives rise to an Arbitrary instance

Equations

• Plausible.instArbitraryOfArbitraryFueled = { arbitrary := Plausible.Gen.sized Plausible.ArbitraryFueled.arbitraryFueled }

def Plausible.Gen.outOfFuel : GenError

Raised when a fueled generator fails due to insufficient fuel.

Equations

• Plausible.Gen.outOfFuel = Plausible.GenError.genError "out of fuel"