vector

Vec

data Vec (A : Type) : Nat -> Type

A list of exactly n elements of A.

Vec.head

def head {A : Type} {n : Nat} (v : Vec A (succ n)) : A

The first element of a non-empty vector.

Vec.tail

def tail {A : Type} {n : Nat} (v : Vec A (succ n)) : Vec A n

A non-empty vector without its first element.

Vec.toList

def toList {A : Type} {n : Nat} (v : Vec A n) : List A

The elements as a list, in order.

Vec.fromList

def fromList {A : Type} (xs : List A) : Vec A (List.length xs)

A list as a vector of its length.

Vec.map

def map {A : Type} {B : Type} {n : Nat} (f : A -> B) (v : Vec A n) : Vec B n

f applied to every element.

Vec.replicate

def replicate {A : Type} (n : Nat) (x : A) : Vec A n

n copies of x.

Vec.append

def append {A : Type} {m : Nat} {n : Nat} (a : Vec A m) (b : Vec A n) : Vec A (add m n)

The elements of a, then those of b.

Vec.zipWith

def zipWith {A : Type} {B : Type} {C : Type} {n : Nat} (f : A -> B -> C) (a : Vec A n) (b : Vec B n) : Vec C n

f applied to the elements at the same positions of two vectors of the same length.

Vec.foldRight

def foldRight {A : Type} {B : Type} {n : Nat} (f : A -> B -> B) (z : B) (v : Vec A n) : B

The elements folded from the last to the first: f x rest.

Vec.get

def get {A : Type} {n : Nat} (v : Vec A n) (i : Fin n) : A

The element at an index (Fin n cannot be out of range: there is no index into vnil).

Vec.tabulate

def tabulate {A : Type} (n : Nat) (f : Fin n -> A) : Vec A n

The vector of f at every index, in order.

Vec.toListLength

def toListLength {A : Type} {n : Nat} (v : Vec A n) : List.length (toList v) = n

The list of a vector has the length the type gives.

Vec.mapToList

def mapToList {A : Type} {B : Type} {n : Nat} (f : A -> B) (v : Vec A n) : toList (map f v) = List.map f (toList v)

Mapping a vector, then taking its list, is mapping its list.

Vec.appendToList

def appendToList {A : Type} {m : Nat} {n : Nat} (a : Vec A m) (b : Vec A n) : toList (append a b) = List.append (toList a) (toList b)

The list of an appended vector is the appended lists.

Vec.fromListToList

def fromListToList {A : Type} (xs : List A) : toList (fromList xs) = xs

A list’s vector gives the list back.