Idris2Doc : Data.NumIdr.Transform.Point

Data.NumIdr.Transform.Point

(source)
Definitions
record Point : Nat -> Type -> Type
  A point is a wrapper around the basic vector type, intended to be used with
  `Transform`. These contain the exact same information as a vector, but
  behave differently when transforms are applied to them.

  Totality: total
  Visibility: export
  Constructor: 
MkPoint : Vector n a -> Point n a

  Projection: 
.vec : Point n a -> Vector n a

  Hints:
  
Applicative (Point n)
  
Cast a b => Cast (Point n a) (Point n b)
  
Foldable (Point n)
  
Functor (Point n)
  
Monad (Point n)
  
Num a => Mult (Matrix m n a) (Point n a) (Point m a)
  
Num a => Mult (Transform ty n a) (Point n a) (Point n a)
  
Show a => Show (Point n a)
  
Traversable (Point n)
  
Zippable (Point n)
fromVector : Vector n a -> Point n a
  Construct a point from a vector.

  Totality: total
  Visibility: export
toVector : Point n a -> Vector n a
  Convert a point to a vector.

  Totality: total
  Visibility: export
point : Vect n a -> Point n a
  Construct a point given its coordinates.

  Totality: total
  Visibility: export
origin : Num a => Point n a
  The origin point.

  Totality: total
  Visibility: export
index : Fin n -> Point n a -> a
  Index the point at the given coordinate.

  Totality: total
  Visibility: export
(!!) : Point n a -> Fin n -> a
  Index the point 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 -> Point n a -> Maybe a
  Index the point at the given coordinate, returning `Nothing` if the index
  is out of bounds.

  Totality: total
  Visibility: export
(!?) : Point n a -> Nat -> Maybe a
  Index the point at the given coordinate, returning `Nothing` if the index
  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
toVect : Point n a -> Vect n a
  Return a `Vect` of the coordinates in the point.

  Totality: total
  Visibility: export
.x : Point (1 + n) a -> a
  Return the x-coordinate (the first value) of the vector.

  Totality: total
  Visibility: export
.y : Point (2 + n) a -> a
  Return the y-coordinate (the second value) of the vector.

  Totality: total
  Visibility: export
.z : Point (3 + n) a -> a
  Return the z-coordinate (the third value) of the vector.

  Totality: total
  Visibility: export
(+.) : Num a => Vector n a -> Point n a -> Point n a
  Add a vector to a point.

  Totality: total
  Visibility: export
  Fixity Declaration: infixr operator, level 8
(.+) : Num a => Point n a -> Vector n a -> Point n a
  Add a point to a vector.

  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 8
(-.) : Neg a => Point n a -> Point n a -> Vector n a
  Subtract two points to get the vector between them.

  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 8