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

instance Plausible.Rat.shrinkable : Shrinkable Rat

Equations

• One or more equations did not get rendered due to their size.

instance Plausible.PNat.shrinkable : Shrinkable ℕ+

Equations

• Plausible.PNat.shrinkable = { shrink := fun (m : ℕ+) => List.map Nat.succPNat (Plausible.Nat.shrink m.natPred) }

instance Plausible.Rat.sampleableExt : SampleableExt Rat

Equations

• One or more equations did not get rendered due to their size.

instance Plausible.PNat.sampleableExt : SampleableExt ℕ+

Equations

• Plausible.PNat.sampleableExt = Plausible.SampleableExt.mkSelfContained do let n ← Plausible.Gen.chooseNat pure n.succPNat