fact: Definition toF (x : type) : float radix := match x with | Fnan => Basic.Fnan | Float m e => match mantissa_sign m with | Mzero => Basic.Fzero | Mnumber s p => Basic.Float s (MtoP p) (EtoZ e) end end.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig