fact: Definition merge_float2_func t := match t with | reInteger x => merge_float2_aux x 0 | reUnary uoNeg (reFloat2 x y) => merge_float2_aux (- x) y | reBinary boMul (reFloat2 x1 y1) (reFloat2 x2 y2) => merge_float2_aux (x1 * x2) (y1 + y2) | reFloat2 x y => merge_float2_aux x y | _ => t end.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library