@[implicit_reducible]

instance Vector.shrinkable {α : Type u_1} [Plausible.Shrinkable α] {n : Nat} : Plausible.Shrinkable (Vector α n)

Equations

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

@[implicit_reducible]

instance Vector.Arbitrary {n : Nat} {α : Type u_1} [Plausible.Arbitrary α] : Plausible.Arbitrary (Vector α n)

Equations

• Vector.Arbitrary = { arbitrary := Vector.ofFnM fun (x : Fin n) => Plausible.Arbitrary.arbitrary }

@[implicit_reducible]

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

Equations

• Fin.shrinkableNat = { shrink := fun (m : Fin n) => List.filterMap (fun (k : Nat) => if h : k < n then some ⟨k, h⟩ else none) (Plausible.Nat.shrink ↑m) }

@[implicit_reducible]

instance Fin.arbitraryNat {n : Nat} : Plausible.Arbitrary (Fin n)

Equations

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