OrienRepr.MathBase

From FinMatrix Require Export MatrixR.
Require Export Reals.

Open Scope nat_scope.
Open Scope R_scope.
Open Scope vec_scope.
Open Scope mat_scope.

Convert a angle between degree and radian

Inductive AngleKind := Radian | Degree.

Definition deg2rad (d : R) : R := d * PI / 180.
Definition rad2deg (r : R) : R := r * 180 / PI.

Record angle := {
    angle_radian : R;
    angle_degree : R
  }.

Definition mk_angle_deg (d : R) : angle :=
  Build_angle (deg2rad d) d.

Definition mk_angle_rad (r : R) : angle :=
  Build_angle r (rad2deg r).

Notation "r 'rad" := (mk_angle_rad r) (at level 30).
Notation "d 'deg" := (mk_angle_deg d) (at level 30).

Section test.
  Goal 180 'deg = PI 'rad.
  Proof. cbv. f_equal; field. ra. Qed.
End test.