Given an example x : α, Shrinkable α gives us a way to shrink it
and suggest simpler examples.
- shrink (x : α) : List α
Instances
@[implicit_reducible]
instance
Plausible.instShrinkableSum
{α : Type u_1}
{β : Type u_2}
[Shrinkable α]
[Shrinkable β]
:
Shrinkable (α ⊕ β)
@[irreducible]
Nat.shrink' n creates a list of smaller natural numbers by
successively dividing n by 2 . For example, Nat.shrink 5 = [2, 1, 0].
Instances For
@[implicit_reducible]
Int.shrinkable operates like Nat.shrinkable but also includes the negative variants.
@[implicit_reducible]
@[implicit_reducible]
instance
Plausible.Prod.shrinkable
{α : Type u_1}
{β : Type u_2}
[shrA : Shrinkable α]
[shrB : Shrinkable β]
:
Shrinkable (α × β)
@[implicit_reducible]
instance
Plausible.Sigma.shrinkable
{α : Type u_1}
{β : Type u_2}
[shrA : Shrinkable α]
[shrB : Shrinkable β]
:
Shrinkable ((_ : α) × β)
@[implicit_reducible]
Shrink a list of a shrinkable type, either by discarding an element or shrinking an element.
@[implicit_reducible]
@[implicit_reducible]
@[implicit_reducible]
instance
Plausible.Subtype.shrinkable
{α : Type u}
{β : α → Prop}
[Shrinkable α]
[(x : α) → Decidable (β x)]
:
Shrinkable { x : α // β x }