Library Flocq.Flocq_version
Library Flocq.Core.Fcore_Raux
Library Flocq.Core.Fcore_Zaux
Library Flocq.Core.Fcore_defs
Library Flocq.Core.Fcore_digits
Library Flocq.Core.Fcore_float_prop
Library Flocq.Core.Fcore_FIX
Library Flocq.Core.Fcore_FLT
Library Flocq.Core.Fcore_FLX
Library Flocq.Core.Fcore_FTZ
Library Flocq.Core.Fcore_generic_fmt
Library Flocq.Core.Fcore_rnd
Library Flocq.Core.Fcore_rnd_ne
Library Flocq.Core.Fcore_ulp
Library Flocq.Core.Fcore
Library Flocq.Calc.Fcalc_bracket
Library Flocq.Calc.Fcalc_digits
Library Flocq.Calc.Fcalc_div
Library Flocq.Calc.Fcalc_ops
Library Flocq.Calc.Fcalc_round
- Helper function for computing the rounded value of a real number.
- Instances of the theorems above, for the usual rounding modes.
Library Flocq.Calc.Fcalc_sqrt
Library Flocq.Prop.Fprop_div_sqrt_error
Library Flocq.Prop.Fprop_mult_error
Library Flocq.Prop.Fprop_plus_error
Library Flocq.Prop.Fprop_relative
Library Flocq.Prop.Fprop_Sterbenz
Library Flocq.Appli.Fappli_rnd_odd
Library Flocq.Appli.Fappli_IEEE
Library Flocq.Appli.Fappli_IEEE_bits
Library Flocq.Appli.Fappli_double_round
This page has been generated by coqdoc