Data.NumIdr.Transform.Rotation

Definitions

Rotation : Nat -> Type -> Type

  A transform that contains a rotation.

Totality: total
Visibility: public export

isRotation' : FieldCmp a => Matrix' n a -> Bool

  Determine if a matrix represents a rotation.

Totality: total
Visibility: export

fromMatrix : FieldCmp a => Matrix' n a -> Maybe (Rotation n a)

  Try to constuct a rotation from a matrix.

Totality: total
Visibility: export

isRotation : FieldCmp a => HMatrix' n a -> Bool

  Determine if a homogeneous matrix represents a rotation.

Totality: total
Visibility: export

fromHMatrix : FieldCmp a => HMatrix' n a -> Maybe (Rotation n a)

Totality: total
Visibility: export

rotate2D : Num a => Double -> Rotation 2 Double

  Construct a 2D rotation that rotates by the given angle (in radians).

Totality: total
Visibility: export

rotate3DX : Double -> Rotation 3 Double

  Construct a 3D rotation around the x-axis.

Totality: total
Visibility: export

rotate3DY : Double -> Rotation 3 Double

  Construct a 3D rotation around the y-axis.

Totality: total
Visibility: export

rotate3DZ : Double -> Rotation 3 Double

  Construct a 3D rotation around the z-axis.

Totality: total
Visibility: export

faceTowards : Vector 3 Double -> Vector 3 Double -> Rotation 3 Double

  Construct a rotation representing an observer facing towards `dir`.
  
  @ dir The facing direction, aligned with the z-axis.
  @ up The vertical direction, the direction that the y-axis faces.

Totality: total
Visibility: export