Instances for Plausible

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

import LeanPool.Apportionment
import Plausible

/-!
# LeanPool.Apportionment.PlausibleInstances

Imported Lean Pool material for `LeanPool.Apportionment.PlausibleInstances`.
-/

open Apportionment

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

#sample Election 2

@[implicit_reducible]

instance Apportionment.shrinkableVector {n : ℕ} : Plausible.Shrinkable (Vector ℕ n)

Equations

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

@[implicit_reducible]

instance Apportionment.shrinkablePNat : Plausible.Shrinkable ℕ+

Equations

• Apportionment.shrinkablePNat = { shrink := fun (n : ℕ+) => List.filterMap (fun (m : ℕ) => if h : 0 < m then some ⟨m, h⟩ else none) (Plausible.Shrinkable.shrink ↑n) }

@[implicit_reducible]

instance Apportionment.arbitraryPNat : Plausible.Arbitrary ℕ+

Equations

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

@[implicit_reducible]

instance Apportionment.shrinkableElection {n : ℕ} : Plausible.Shrinkable (Election n)

Equations

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

@[implicit_reducible]

instance Apportionment.arbitraryElection {n : ℕ} [NeZero n] : Plausible.Arbitrary (Election n)

Equations

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

@[implicit_reducible]

instance Apportionment.sampleableElection {n : ℕ} [NeZero n] : Plausible.SampleableExt (Election n)

Equations

• Apportionment.sampleableElection = Plausible.SampleableExt.selfContained