CoRN.examples.PlotExamples

Require Import Plot.
Require Import CRtrans.

Notation star := (@refl_equal _ Lt).
Notation "∗" := star.

Open Local Scope Q_scope.
Open Local Scope uc_scope.
Open Local Scope raster.

Time Eval vm_compute in PlotQ (- (3)) 3 star (- (1)) 1 star sin_uc 36 12.

Goal True.
assert (X:=@Plot_correct (-(3)) 0 star 0 1 star
 (exp_bound_uc 0)
 45 15 refl_equal refl_equal).
match goal with
 [X:ball ?e ?a (@ucFun _ _ _ (_⇱?b⇲_))|-_] ⇒ set (E:=e) in X; set (B:=b) in X
end.
set (E' := E: Q).
vm_compute in E'.
Time vm_compute in B.
unfold E, B in X.
clear E B.
split.
Qed.