Theorems · Definition · combinatorics

List.Vector

Type u → ℕ → Type (max 0 u)

List.Vector α n is the type of lists of length n with elements of type α. Note that there is also Vector α n in the root namespace, which is the type of arrays of length n with elements of type α. Typically, if you are doing programming or verification, you will primarily use Vector α n, and if you are doing mathematics, you may want to use List.Vector α n instead.

Defined in

Mathlib.Data.Vector.Defs

Cited by

270 results in Mathlib

Foundations

Depth 10 from the axioms, rests on 33 definitions · uses no axioms