Data.NumIdr.Vector

Reexports

Definitions

Vector : Nat -> Type -> Type

  A vector is a rank-1 array.

Totality: total
Visibility: public export

dim : Vector n a -> Nat

  The length (number of dimensions) of the vector.

Totality: total
Visibility: public export

dimEq : (v : Vector n a) -> n = dim v

Totality: total
Visibility: export

vector : {default B rep : Rep} -> RepConstraint rep a => Vect n a -> Vector n a

  Construct a vector from a `Vect`.

Totality: total
Visibility: export

toVect : Vector n a -> Vect n a

  Convert a vector into a `Vect`.

Totality: total
Visibility: export

basis : {default B rep : Rep} -> RepConstraint rep a => Num a => Fin n -> Vector n a

  Return the `i`-th basis vector.

Totality: total
Visibility: export

basisX : {default B rep : Rep} -> RepConstraint rep a => Num a => Vector (1 + n) a

  The first basis vector.

Totality: total
Visibility: export

basisY : {default B rep : Rep} -> RepConstraint rep a => Num a => Vector (2 + n) a

  The second basis vector.

Totality: total
Visibility: export

basisZ : {default B rep : Rep} -> RepConstraint rep a => Num a => Vector (3 + n) a

  The third basis vector.

Totality: total
Visibility: export

unit2D : {default B rep : Rep} -> RepConstraint rep Double => Double -> Vector 2 Double

  Calculate the 2D unit vector with the given angle off the x-axis.

Totality: total
Visibility: export

unit3D : {default B rep : Rep} -> RepConstraint rep Double => Double -> Double -> Vector 3 Double

  Calculate the 3D unit vector corresponding to the given spherical coordinates,
  where the polar axis is the z-axis.
  
  @ pol The polar angle of the vector
  @ az  The azimuthal angle of the vector

Totality: total
Visibility: export

index : Fin n -> Vector n a -> a

  Index the vector at the given coordinate.

Totality: total
Visibility: export

(!!) : Vector n a -> Fin n -> a

  Index the vector at the given coordinate.
  
  This is the operator form of `index`.

Totality: total
Visibility: export
Fixity Declarations:
infixl operator, level 10
infixl operator, level 10
infixl operator, level 10

indexNB : Nat -> Vector n a -> Maybe a

  Index the vector at the given coordinate, returning `Nothing` if the
  coordinate is out of bounds.

Totality: total
Visibility: export

(!?) : Vector n a -> Nat -> Maybe a

  Index the vector at the given coordinate, returning `Nothing` if the
  coordinate is out of bounds.
  
  This is the operator form of `indexNB`.

Totality: total
Visibility: export
Fixity Declarations:
infixl operator, level 10
infixl operator, level 10
infixl operator, level 10

.x : Vector (1 + n) a -> a

  Return the x-coordinate (the first value) of the vector.

Totality: total
Visibility: export

.y : Vector (2 + n) a -> a

  Return the y-coordinate (the second value) of the vector.

Totality: total
Visibility: export

.z : Vector (3 + n) a -> a

  Return the z-coordinate (the third value) of the vector.

Totality: total
Visibility: export

swizzle : Vect n (Fin m) -> Vector m a -> Vector n a

  Construct a vector by pulling coordinates from another vector.

Totality: total
Visibility: export

swapCoords : Fin n -> Fin n -> Vector n a -> Vector n a

  Swap two coordinates in a vector.

Totality: total
Visibility: export

permuteCoords : Permutation n -> Vector n a -> Vector n a

  Permute the coordinates in a vector.

Totality: total
Visibility: export

(++) : Vector m a -> Vector n a -> Vector (m + n) a

  Concatenate one vector with another.

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

dot : Num a => Vector n a -> Vector n a -> a

  Calculate the dot product of the two vectors.

Totality: total
Visibility: export

perp : Neg a => Vector 2 a -> Vector 2 a -> a

  Calculate the perpendicular product of the two vectors.

Totality: total
Visibility: export

cross : Neg a => Vector 3 a -> Vector 3 a -> Vector 3 a

  Calculate the cross product of the two vectors.

Totality: total
Visibility: export

triple : Neg a => Vector 3 a -> Vector 3 a -> Vector 3 a -> a

  Calculate the triple product of the three vectors.

Totality: total
Visibility: export