Data.Matrix

Definitions

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

Totality: total
Visibility: export
Constructor: 

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

Hints:

Eq a => Eq (Matrix rows cols a)

Functor (Matrix rows cols)

Show a => Show (Matrix rows cols a)

Zippable (Matrix rows cols)

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

Visibility: public export

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

Visibility: public export

fill : (rows : Nat) -> (cols : Nat) -> t -> Matrix rows cols t

Visibility: public export

zeros : (rows : Nat) -> (cols : Nat) -> Matrix rows cols Int

Visibility: public export

ones : (rows : Nat) -> (cols : Nat) -> Matrix rows cols Int

Visibility: public export

updateAt : Fin rows -> Fin cols -> (a -> a) -> Matrix rows cols a -> Matrix rows cols a

Visibility: public export

replaceAt : Fin rows -> Fin cols -> ele -> Matrix rows cols ele -> Matrix rows cols ele

Visibility: public export

findIndex : (ele -> Bool) -> Matrix rows cols ele -> Maybe (Fin rows, Fin cols)

Visibility: public export

mapWithIndex : {auto rows : Nat} -> {auto cols : Nat} -> (ele -> (Fin rows, Fin cols) -> b) -> Matrix rows cols ele -> Matrix rows cols b

Visibility: public export

findIndices : {auto rows : Nat} -> {auto cols : Nat} -> (ele -> Bool) -> Matrix rows cols ele -> List (Fin rows, Fin cols)

Visibility: public export

eye : (rows : Nat) -> (cols : Nat) -> Matrix rows cols Int

Visibility: public export

identity : (rows : Nat) -> Matrix rows rows Int

Visibility: public export

repmat : Num ele => Vect n ele -> (rows : Nat) -> (cols : Nat) -> Matrix rows (cols * n) ele

Visibility: public export

(+) : Num n => Matrix rows cols n -> Matrix rows cols n -> Matrix rows cols n

Visibility: public export
Fixity Declaration: infixl operator, level 8

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 n => Matrix rows cols n -> Matrix rows cols n -> Matrix rows cols n

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

scalarMulti : Num a => a -> Matrix rows cols a -> Matrix rows cols a

Visibility: public export

transpose : Matrix rows cols n -> Matrix cols rows n

Visibility: public export

(*) : Num a => Matrix m l a -> Matrix l n a -> Matrix m n a

Visibility: public export
Fixity Declaration: infixl operator, level 9

minor : Fin (S n) -> Fin (S n) -> Matrix (S n) (S n) a -> Matrix n n a

Visibility: public export

algeCofactor : Neg a => Fin (S n) -> Fin (S n) -> Matrix (S n) (S n) a -> Matrix n n a

Visibility: public export

trace : Num a => Matrix n n a -> a

Visibility: public export

flipVer : Matrix m n a -> Matrix m n a

Visibility: export

flipHor : Matrix m n a -> Matrix m n a

Visibility: export