mathlib3 documentation

logic.small.list

Instances for small (list α) and small (vector α). #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
@[protected, instance]
def small_vector {α : Type v} {n : ℕ} [small α] :
small (vector α n)
source
@[protected, instance]
def small_list {α : Type v} [small α] :
small (list α)