diff options
Diffstat (limited to 'contrib/extraction/test/custom/Reals.v')
| -rw-r--r-- | contrib/extraction/test/custom/Reals.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/contrib/extraction/test/custom/Reals.v b/contrib/extraction/test/custom/Reals.v new file mode 100644 index 00000000..45d0a224 --- /dev/null +++ b/contrib/extraction/test/custom/Reals.v @@ -0,0 +1,17 @@ +Require Import Reals. +Extract Inlined Constant R => float. +Extract Inlined Constant R0 => "0.0". +Extract Inlined Constant R1 => "1.0". +Extract Inlined Constant Rplus => "(+.)". +Extract Inlined Constant Rmult => "( *.)". +Extract Inlined Constant Ropp => "(~-.)". +Extract Inlined Constant Rinv => "(fun x -> 1.0 /. x)". +Extract Inlined Constant Rlt => "(<)". +Extract Inlined Constant up => "AddReals.my_ceil". +Extract Inlined Constant total_order_T => "AddReals.total_order_T". +Extract Inlined Constant sqrt => "sqrt". +Extract Inlined Constant sigma => "(fun l h -> sigma_aux l h (Minus.minus h l))". +Extract Inlined Constant PI => "3.141593". +Extract Inlined Constant cos => cos. +Extract Inlined Constant sin => sin. +Extract Inlined Constant derive_pt => "(fun f x -> ((f (x+.1E-5))-.(f x))*.1E5)". |