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 α

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Plausible.Unit.shrinkable : Shrinkable Unit

Equations

• Plausible.Unit.shrinkable = { }

@[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].

Equations

• Plausible.Nat.shrink n = if 0 < n then have m := n / 2; m :: Plausible.Nat.shrink m else []

@[implicit_reducible]

instance Plausible.Nat.shrinkable : Shrinkable Nat

Equations

• Plausible.Nat.shrinkable = { shrink := Plausible.Nat.shrink }

@[implicit_reducible]

instance Plausible.Fin.shrinkable {n : Nat} : Shrinkable (Fin n.succ)

Equations

• Plausible.Fin.shrinkable = { shrink := fun (m : Fin n.succ) => List.map (Fin.ofNat n.succ) (Plausible.Nat.shrink ↑m) }

@[implicit_reducible]

instance Plausible.BitVec.shrinkable {n : Nat} : Shrinkable (BitVec n)

Equations

• Plausible.BitVec.shrinkable = { shrink := fun (m : BitVec n) => List.map (BitVec.ofNat n) (Plausible.Nat.shrink m.toNat) }

@[implicit_reducible]

instance Plausible.UInt8.shrinkable : Shrinkable UInt8

Equations

• Plausible.UInt8.shrinkable = { shrink := fun (m : UInt8) => List.map UInt8.ofNat (Plausible.Nat.shrink m.toNat) }

@[implicit_reducible]

instance Plausible.UInt16.shrinkable : Shrinkable UInt16

Equations

• Plausible.UInt16.shrinkable = { shrink := fun (m : UInt16) => List.map UInt16.ofNat (Plausible.Nat.shrink m.toNat) }

@[implicit_reducible]

instance Plausible.UInt32.shrinkable : Shrinkable UInt32

Equations

• Plausible.UInt32.shrinkable = { shrink := fun (m : UInt32) => List.map UInt32.ofNat (Plausible.Nat.shrink m.toNat) }

@[implicit_reducible]

instance Plausible.UInt64.shrinkable : Shrinkable UInt64

Equations

• Plausible.UInt64.shrinkable = { shrink := fun (m : UInt64) => List.map UInt64.ofNat (Plausible.Nat.shrink m.toNat) }

@[implicit_reducible]

instance Plausible.USize.shrinkable : Shrinkable USize

Equations

• Plausible.USize.shrinkable = { shrink := fun (m : USize) => List.map USize.ofNat (Plausible.Nat.shrink m.toNat) }

@[implicit_reducible]

instance Plausible.Int.shrinkable : Shrinkable Int

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

Equations

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

@[implicit_reducible]

instance Plausible.Bool.shrinkable : Shrinkable Bool

Equations

• Plausible.Bool.shrinkable = { }

@[implicit_reducible]

instance Plausible.Char.shrinkable : Shrinkable Char

Equations

• Plausible.Char.shrinkable = { }

@[implicit_reducible]

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

Equations

• Plausible.Option.shrinkable = { shrink := fun (o : Option α) => match o with | some x => List.map some (Plausible.Shrinkable.shrink x) | none => [] }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_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.

Equations

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

@[implicit_reducible]

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

Equations

• Plausible.ULift.shrinkable = { shrink := fun (u : ULift α) => List.map ULift.up (Plausible.Shrinkable.shrink u.down) }

@[implicit_reducible]

instance Plausible.String.shrinkable : Shrinkable String

Equations

• Plausible.String.shrinkable = { shrink := fun (s : String) => List.map String.ofList (Plausible.Shrinkable.shrink s.toList) }

@[implicit_reducible]

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

Equations

• Plausible.Array.shrinkable = { shrink := fun (xs : Array α) => List.map Array.mk (Plausible.Shrinkable.shrink xs.toList) }

@[implicit_reducible]

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

Equations

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