ROSCOQ.CartAR

Require Export CoRN.reals.faster.ARtrans.
Require Export CoRN.reals.fast.CRtrans.
Require Export CoRN.reals.faster.ARbigD.
Require Export CoRN.ftc.IntegrationRules.
Require Export Coq.Program.Tactics.

Definition R2QPrec : Qpos := QposMake 1 100.

Definition threeBy2 : bigD .
exact ((inject_Z_bigD 3) ≪ (-1)).
Defined.

Definition val : ARbigD .
exact ('threeBy2×ARpi).
Defined.

Eval vm_compute in (cast bigD Q (approximate val R2QPrec)).

Definition crNum : CR := ((('(3#2)%Q)*CRpi)).
Eval vm_compute in (approximate crNum R2QPrec).

Instance CastQAR : Cast Q ARbigD := (cast CR AR) ∘ (cast Q CR).

Eval vm_compute in (approximate (cast Q CR (3#2)%Q) R2QPrec).

Eval vm_compute in (cast bigD Q (approximate (cast Q ARbigD (3#2)%Q) R2QPrec)).

Instance Positive2Z : Cast positive Z := Zpos.