Matrix

Reexports

Definitions

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

Totality: total
Visibility: public export
Constructor: 

MkMat : Vect rows (Vect cols a) -> Matrix rows cols a

Projection: 

.contents : Matrix rows cols a -> Vect rows (Vect cols a)

Hints:

Functor (Matrix r c)

Num a => Num (Matrix r c a)

Show a => Show (Matrix r c a)

.contents : Matrix rows cols a -> Vect rows (Vect cols a)

Visibility: public export

contents : Matrix rows cols a -> Vect rows (Vect cols a)

Visibility: public export

colVect : Vect n a -> Matrix n 1 a

  Convert a vector to a column matrix

Visibility: export

rowVect : Vect n a -> Matrix 1 n a

  Convert a vector to a row matrix

Visibility: export

zeros : Num a => Matrix r c a

  Create a matrix of any size with all elements set to zero

Visibility: export

ones : Num a => Matrix r c a

  Create a matrix of any size with all elements set to one

Visibility: export

index : Fin r -> Fin c -> Matrix r c a -> a

  Retreive a value from a matrix

Visibility: export

set : Fin r -> Fin c -> a -> Matrix r c a -> Matrix r c a

  Set a value in a matrix

Visibility: export

identity : Num a => Matrix size size a

  The identity matrix. Both dimensions are the same size.

Visibility: export

transpose : Matrix r c a -> Matrix c r a

  Transpose a matrix

Visibility: export

(><) : Num a => Matrix r1 c1 a -> Matrix r2 c2 a -> Matrix (r1 * r2) (c1 * c2) a

  Tensor product of two matrices

Visibility: export
Fixity Declaration: infixl operator, level 9

.scale : Num a => Matrix r c a -> a -> Matrix r c a

  Scale a matrix by a scalar

Visibility: export

negate : Neg ty => ty -> ty

  The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 10

(-) : Neg a => Matrix r c a -> Matrix r c a -> Matrix r c a

Visibility: export
Fixity Declarations:
infixl operator, level 8
infixl operator, level 8
prefix operator, level 10

dotProduct : Num a => Vect n a -> Vect n a -> a

Visibility: export

matmul : Num a => Matrix r1 c1 a -> Matrix c1 n a -> Matrix r1 n a

  Standard matrix multiplication

Visibility: export