Idris2Doc : Data.NumIdr.Transform.Translation

Data.NumIdr.Transform.Translation

(source)

Definitions

Translation : Nat->Type->Type
  A translation is a transform that adds a constant vector value
to its input point.

Totality: total
Visibility: public export
isTranslation : Eqa=>Numa=>HMatrix'na->Bool
  Determine if a homogeneous matrix encodes a translation.

Totality: total
Visibility: export
fromHMatrix : Eqa=>Numa=>HMatrix'na->Maybe (Translationna)
  Try to construct a translation from a homogeneous matrix.

Totality: total
Visibility: export
translate : Numa=>Vectorna->Translationna
  Construct a translation given a vector.

Totality: total
Visibility: export