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

@[instance_reducible]

instance Plausible.Rat.shrinkable : Shrinkable Rat

Equations

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

@[instance_reducible]

instance Plausible.PNat.shrinkable : Shrinkable ℕ+

Equations

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

@[instance_reducible]

instance Plausible.Rat.Arbitrary : Plausible.Arbitrary Rat

Equations

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

@[instance_reducible]

instance Plausible.Rat.sampleableExt : SampleableExt Rat

Equations

• Plausible.Rat.sampleableExt = inferInstance

@[instance_reducible]

instance Plausible.PNat.Arbitrary : Plausible.Arbitrary ℕ+

Equations

• Plausible.PNat.Arbitrary = { arbitrary := do let n ← Plausible.Gen.chooseNat pure n.succPNat }

@[instance_reducible]

instance Plausible.PNat.sampleableExt : SampleableExt ℕ+

Equations

• Plausible.PNat.sampleableExt = inferInstance