Instances for Small (List α) and Small (Vector α).

These must not be in Logic.Small.Basic as this is very low in the import hierarchy, and is used by category theory files which do not need everything imported by Data.Vector.Basic.

instance smallVector {α : Type v} {n : ℕ} [Small.{u, v} α] : Small.{u, v} (Vector α n)

Equations

• (_ : Small.{u, v} (Vector α n)) = (_ : Small.{u, v} (Vector α n))

instance smallList {α : Type v} [Small.{u, v} α] : Small.{u, v} (List α)

Equations

• (_ : Small.{u, v} (List α)) = (_ : Small.{u, v} (List α))