blob: b817c360087e1e6a4264139b638fe663efe1024a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Require 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.
|
