Documentation

Apportionmentlib.PlausibleInstances

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
source
@[instance_reducible]
instance Apportionmentlib.instShrinkableVectorNat {n : ℕ} :
Plausible.Shrinkable (Vector ℕ n)
Equations
  • One or more equations did not get rendered due to their size.
source
@[instance_reducible]
instance Apportionmentlib.instShrinkableElection {n : ℕ} :
Plausible.Shrinkable (Election n)
Equations
  • One or more equations did not get rendered due to their size.
source
@[instance_reducible]
instance Apportionmentlib.instArbitraryElectionOfNeZeroNat {n : ℕ} [NeZero n] :
Plausible.Arbitrary (Election n)
Equations
  • One or more equations did not get rendered due to their size.
source
@[instance_reducible]
instance Apportionmentlib.instSampleableExtElectionOfNeZeroNat {n : ℕ} [NeZero n] :
Plausible.SampleableExt (Election n)
Equations