Documentation

Mathlib.Testing.Plausible.Sampleable

This module contains Plausible.Shrinkable and Plausible.SampleableExt instances for mathlib types.

source
@[implicit_reducible]
instance Plausible.Rat.shrinkable :
Shrinkable Rat
source
@[implicit_reducible]
instance Plausible.PNat.shrinkable :
Shrinkable ℕ+
source
@[implicit_reducible]
instance Plausible.Rat.Arbitrary :
Plausible.Arbitrary Rat
source
@[implicit_reducible]
instance Plausible.Rat.sampleableExt :
SampleableExt Rat
source
@[implicit_reducible]
instance Plausible.PNat.Arbitrary :
Plausible.Arbitrary ℕ+
source
@[implicit_reducible]
instance Plausible.PNat.sampleableExt :
SampleableExt ℕ+