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 {n : ℕ} (e : Election n) (h : 2 < n) : e.votes[0] > e.votes[1] := by
  plausible

#sample Election 2
source
instance Apportionmentlib.instShrinkableVectorNat_apportionmentlib {n : ℕ} :
Plausible.Shrinkable (Vector ℕ n)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Apportionmentlib.instShrinkableElection {n : ℕ} :
Plausible.Shrinkable (Election n)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Apportionmentlib.instArbitraryElection {n : ℕ} :
Plausible.Arbitrary (Election n)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Apportionmentlib.instSampleableExtElection {n : ℕ} :
Plausible.SampleableExt (Election n)
Equations