fact: Definition output (fmt : bool) xi := match xi with | Ibnd xl xu => match F.toF xl, F.toF xu with | Float sl ml el, Float su mu eu => (Some (output_bnd fmt false F.radix sl ml el), Some (output_bnd fmt true F.radix su mu eu)) | Fzero, Float su mu eu => (Some (BInteger 0), Some (output_bnd fmt true F.radix su mu eu)) | Float sl ml el, Fzero => (Some (output_bnd fmt false F.radix sl ml el), Some (BInteger 0)) | Fzero, Fzero => (Some (BInteger 0), Some (BInteger 0)) | Fzero, Basic.Fnan => (Some (BInteger 0), None) | Basic.Fnan, Fzero => (None, Some (BInteger 0)) | Basic.Fnan, Float su mu eu => (None, Some (output_bnd fmt true F.radix su mu eu)) | Float sl ml el, Basic.Fnan => (Some (output_bnd fmt false F.radix sl ml el), None) | Basic.Fnan, Basic.Fnan => (None, None) end | Inan => (None, None) end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval