Plausible.Shrinkable

source

class Plausible.Shrinkable (α : Type u) :

Type u

Given an example x : α, Shrinkable α gives us a way to shrink it and suggest simpler examples.

shrink (x : α) : List α

Instances

source

@[instance_reducible]

instance Plausible.instShrinkableSum {α : Type u_1} {β : Type u_2} [Shrinkable α] [Shrinkable β] :

Shrinkable (α ⊕ β)

source

@[instance_reducible]

instance Plausible.Unit.shrinkable :

Shrinkable Unit

source

@[irreducible]

def Plausible.Nat.shrink (n : Nat) :

List Nat

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

source

@[instance_reducible]

instance Plausible.Nat.shrinkable :

Shrinkable Nat

source

@[instance_reducible]

instance Plausible.Fin.shrinkable {n : Nat} :

Shrinkable (Fin n.succ)

source

@[instance_reducible]

instance Plausible.BitVec.shrinkable {n : Nat} :

Shrinkable (BitVec n)

source

@[instance_reducible]

instance Plausible.UInt8.shrinkable :

Shrinkable UInt8

source

@[instance_reducible]

instance Plausible.UInt16.shrinkable :

Shrinkable UInt16

source

@[instance_reducible]

instance Plausible.UInt32.shrinkable :

Shrinkable UInt32

source

@[instance_reducible]

instance Plausible.UInt64.shrinkable :

Shrinkable UInt64

source

@[instance_reducible]

instance Plausible.USize.shrinkable :

Shrinkable USize

source

@[instance_reducible]

instance Plausible.Int.shrinkable :

Shrinkable Int

Int.shrinkable operates like Nat.shrinkable but also includes the negative variants.

source

@[instance_reducible]

instance Plausible.Bool.shrinkable :

Shrinkable Bool

source

@[instance_reducible]

instance Plausible.Char.shrinkable :

Shrinkable Char

source

@[instance_reducible]

instance Plausible.Option.shrinkable {α : Type u_1} [Shrinkable α] :

Shrinkable (Option α)

source

@[instance_reducible]

instance Plausible.Prod.shrinkable {α : Type u_1} {β : Type u_2} [shrA : Shrinkable α] [shrB : Shrinkable β] :

Shrinkable (α × β)

source

@[instance_reducible]

instance Plausible.Sigma.shrinkable {α : Type u_1} {β : Type u_2} [shrA : Shrinkable α] [shrB : Shrinkable β] :

Shrinkable ((_ : α) × β)

source

@[instance_reducible]

instance Plausible.List.shrinkable {α : Type u_1} [Shrinkable α] :

Shrinkable (List α)

Shrink a list of a shrinkable type, either by discarding an element or shrinking an element.

source

@[instance_reducible]

instance Plausible.ULift.shrinkable {α : Type u_1} [Shrinkable α] :

Shrinkable (ULift α)

source

@[instance_reducible]

instance Plausible.String.shrinkable :

Shrinkable String

source

@[instance_reducible]

instance Plausible.Array.shrinkable {α : Type u_1} [Shrinkable α] :

Shrinkable (Array α)

source

@[instance_reducible]

instance Plausible.Subtype.shrinkable {α : Type u} {β : α → Prop} [Shrinkable α] [(x : α) → Decidable (β x)] :

Shrinkable { x : α // β x }