Instances for Plausible

In this file, we define some instances (like Shrinkable, Arbitrary, SampleableExt) so that you can use the plausible tactic with Apportionmentlib. For example, try:

import Apportionmentlib
import Plausible

open Apportionmentlib

example (e : Election 4) : e.votes[0] ≤ 15 + e.votes[1] := by
  plausible

#sample Election 2

instance Apportionmentlib.instShrinkableVectorNat_apportionmentlib {n : ℕ} : Plausible.Shrinkable (Vector ℕ n)

Equations

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

instance Apportionmentlib.instShrinkablePNat_apportionmentlib : Plausible.Shrinkable ℕ+

Equations

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

instance Apportionmentlib.instArbitraryPNat_apportionmentlib : Plausible.Arbitrary ℕ+

Equations

• Apportionmentlib.instArbitraryPNat_apportionmentlib = { arbitrary := do let __do_lift ← Plausible.Gen.getSize let n ← Plausible.Gen.choose ℕ 1 (__do_lift + 1) ⋯ pure ⟨↑n, ⋯⟩ }

instance Apportionmentlib.instShrinkableElection {n : ℕ} : Plausible.Shrinkable (Election n)

Equations

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

instance Apportionmentlib.instArbitraryElectionOfNeZeroNat {n : ℕ} [NeZero n] : Plausible.Arbitrary (Election n)

Equations

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

instance Apportionmentlib.instSampleableExtElectionOfNeZeroNat {n : ℕ} [NeZero n] : Plausible.SampleableExt (Election n)

Equations

• Apportionmentlib.instSampleableExtElectionOfNeZeroNat = Plausible.SampleableExt.selfContained