Idris2Doc : Data.NumIdr.Transform.Rigid

Data.NumIdr.Transform.Rigid

(source)

Definitions

Rigid : Nat -> Type -> Type
  A rigid transform encodes a (proper) rigid transformation, also known as a
rototranslation.

Totality: total
Visibility: public export
isRigid : FieldCmp a => HMatrix' n a -> Bool
  Determine if a homogeneous matrix represents a rigid transform.

Totality: total
Visibility: export
fromHMatrix : FieldCmp a => HMatrix' n a -> Maybe (Rigid n a)
Totality: total
Visibility: export
rigid2D : Vector 2 Double -> Double -> Rigid 2 Double
Totality: total
Visibility: export
faceTowards : Point 3 Double -> Point 3 Double -> Vector 3 Double -> Rigid 3 Double
  Construct a 3D rigid transform representing an observer standing at `orig`
and facing towards `target`.

@ orig The origin point, i.e. the point that the origin is mapped to.
@ target The point that the z-axis is directed towards.
@ up The vertical direction, the direction that the y-axis faces.

Totality: total
Visibility: export