taylor_rocqs/plot.v at master · holgerthies/taylor_rocqs · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
(* The syntax is "filename:plugin_name" *)
Declare ML Module "plot_plugin.plugin".
Goal True.
plot_start.
(* plot_send constr:("y(t)   = ('-4.26815559±23.8930' :: '-7.2946668±49.6809' :: '29.1249590±17.9049' :: nil)"). *)
(* plot_start. *)
(* plot_send "". *)

(* plot_send "t      = '0.586814904±0.000001993'". *)
(* plot_send "y(t)   = ('-4.26815559±23.8930' :: '-7.2946668±49.6809' :: '29.1249590±17.9049' :: nil)". *)

(* plot_send "t      = '0.686814904±0.000001993'". *)
(* plot_send "y(t)   = ('-4.26815559±23.8930' :: '-7.2946668±49.6809' :: '29.1249590±17.9049' :: nil)". *)

(* plot_send "t      = ""0.686814904±0.000001993""". *)
(* plot_send "y(t)   = (""-4.26815559±23.8930"" :: ""-7.2946668±49.6809"" :: ""29.1249590±17.9049"" :: nil)". *)

(* plot_send "t      = ""1.686814904±0.000001993""". *)
(* plot_send "y(t)   = (""-4.26815559±23.8930"" :: ""-7.2946668±49.6809"" :: ""29.1249590±17.9049"" :: nil)". *)
plot_stop.
  trivial.
Qed.