IdrisDoc: Data.Matrix

Data.Matrix

Basic matrix operations with dimensionalities enforced
at the type level

Matrix : Nat -> Nat -> Type -> Type

Matrix with n rows and m columns

col : Vect n a -> Matrix n (fromInteger 1) a

Cast a vector from a standard Vect to a proper n x 1 matrix

concatMatrix : Matrix n m (Matrix x y a) -> Matrix (n * x) (m * y) a

Flatten a matrix of matrices

deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a

Delete the specified column of a matrix

deleteRow : Fin (S n) -> Matrix (S n) m a -> Matrix n m a

Delete the specified row of a matrix

fins : (n : Nat) -> Vect n (Fin n)

All finite numbers of the specified level

getCol : Fin m -> Matrix n m a -> Vect n a

Get the specified column of a matrix

getRow : Fin n -> Matrix n m a -> Vect m a

Get the specified row of a matrix

indices : Fin n -> Fin m -> Matrix n m a -> a

Matrix element at specified row and column indices

insertCol : Fin (S m) -> Vect n a -> Matrix n m a -> Matrix n (S m) a
insertRow : Fin (S n) -> Vect m a -> Matrix n m a -> Matrix (S n) m a
row : Vect n a -> Matrix (fromInteger 1) n a

Cast a row from a standard Vect to a proper 1 x n matrix

subMatrix : Fin (S n) -> Fin (S m) -> Matrix (S n) (S m) a -> Matrix n m a

Matrix formed by deleting specified row and col