fact: Definition compact_float10 m e := match m with | Z0 => Float10 0 0 | Zpos p => match float10_of_pos p with | Float10 m e1 => Float10 m (e + e1) end | Zneg p => match float10_of_pos p with | Float10 m e1 => Float10 (-m) (e + e1) end end.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library