FinMatrix.CoqExt.MyExtrOCamlR
Require Export Extraction.
Require Import Reals.
Extract Constant R => float.
Extract Constant Rabst => "__".
Extract Constant Rrepr => "__".
Extract Constant R0 => "0.0".
Extract Constant R1 => "1.0".
Extract Constant PI => "Float.pi".
Extract Constant Rplus => "(+.)".
Extract Constant Rmult => "( *. )".
Extract Constant Rminus => "(-.)".
Extract Constant Ropp => "fun a -> (0.0 -. a)".
Extract Constant Rinv => "fun a -> (1.0 /. a)".
Extract Constant Rpower => "Float.pow".
Extract Constant sin => "Float.sin".
Extract Constant cos => "Float.cos".
Extract Constant sqrt => "Float.sqrt".
Extract Constant atan => "Float.atan".
Extract Constant acos => "Float.acos".
two float numbers are comparison decidable
Extract Constant total_order_T => "fun r1 r2 ->
let c = Float.compare r1 r2 in
if c < 0 then Some true
else (if c = 0 then None else Some false)".
Extract Constant Req_dec_T => "fun r1 r2 -> let c = Float.compare r1 r2 in if c = 0 then true else false".
Extract Constant Req_dec_T => "fun r1 r2 -> let c = Float.compare r1 r2 in if c = 0 then true else false".