Commit 659146bb authored by MARCHE Claude's avatar MARCHE Claude
Browse files

coq output: trigonometric functions

parent 3e74ed80
...@@ -16,6 +16,8 @@ transformation "inline_trivial" ...@@ -16,6 +16,8 @@ transformation "inline_trivial"
transformation "eliminate_builtin" transformation "eliminate_builtin"
transformation "eliminate_recursion" transformation "eliminate_recursion"
transformation "eliminate_if"
transformation "simplify_formula" transformation "simplify_formula"
transformation "simplify_trivial_quantification_in_goal" transformation "simplify_trivial_quantification_in_goal"
...@@ -197,12 +199,12 @@ theory real.Trigonometry ...@@ -197,12 +199,12 @@ theory real.Trigonometry
prelude "Require Import Rtrigo." prelude "Require Import Rtrigo."
prelude "Require Import AltSeries. (* for def of pi *)" prelude "Require Import AltSeries. (* for def of pi *)"
syntax logic cos "(cos %1)" syntax logic cos "(Rtrigo_def.cos %1)"
syntax logic sin "(sin %1)" syntax logic sin "(Rtrigo_def.sin %1)"
syntax logic pi "PI" syntax logic pi "PI"
syntax logic tan "(tan %1)" syntax logic tan "(Rtrigo.tan %1)"
(* syntax logic atan "atan not defined in Coq ?" *) (* syntax logic atan "atan not defined in Coq ?" *)
end end
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment