Documentation

Mathlib.Testing.Plausible.Sampleable

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

source
🔸 coverage
@[implicit_reducible]
instance Plausible.Rat.shrinkable :
Shrinkable â„š
source
🔸 coverage
@[implicit_reducible]
instance Plausible.PNat.shrinkable :
Shrinkable â„•+
source
🔸 coverage
@[implicit_reducible]
instance Plausible.Rat.Arbitrary :
Plausible.Arbitrary â„š
source
🔸 coverage
@[implicit_reducible]
instance Plausible.Rat.sampleableExt :
SampleableExt â„š
source
🔸 coverage
@[implicit_reducible]
instance Plausible.PNat.Arbitrary :
Plausible.Arbitrary â„•+
source
🔸 coverage
@[implicit_reducible]
instance Plausible.PNat.sampleableExt :
SampleableExt â„•+