Flocq

Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1194 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (20 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (15 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (10 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (650 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (78 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (42 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (41 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (19 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (172 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (119 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (28 entries)

Global Index

A

abs_round_ge_generic [lemma, in Flocq.Core.Fcore_generic_fmt]
abs_cond_Zopp [lemma, in Flocq.Core.Fcore_Raux]
abs_B2R_lt_emax [lemma, in Flocq.Appli.Fappli_IEEE]
abs_round_le_generic [lemma, in Flocq.Core.Fcore_generic_fmt]
abs_lt_bpow_prec [lemma, in Flocq.Core.Fcore_generic_fmt]
abs_cond_Ropp [lemma, in Flocq.Core.Fcore_Raux]
AnyRadix [section, in Flocq.Appli.Fappli_IEEE]


B

Bdiv [definition, in Flocq.Appli.Fappli_IEEE]
Bdiv_correct [lemma, in Flocq.Appli.Fappli_IEEE]
Bdiv_correct_aux [lemma, in Flocq.Appli.Fappli_IEEE]
Binary [section, in Flocq.Appli.Fappli_IEEE]
Binary_Bits.prec [variable, in Flocq.Appli.Fappli_IEEE_bits]
binary_normalize [definition, in Flocq.Appli.Fappli_IEEE]
binary_float_of_bits_of_binary_float [lemma, in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.Hmax [variable, in Flocq.Appli.Fappli_IEEE_bits]
binary_round [definition, in Flocq.Appli.Fappli_IEEE]
Binary_Bits.Hew [variable, in Flocq.Appli.Fappli_IEEE_bits]
binary_float_of_bits_aux [definition, in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits [section, in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.ew [variable, in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.emax [variable, in Flocq.Appli.Fappli_IEEE_bits]
binary_round_aux [definition, in Flocq.Appli.Fappli_IEEE]
binary_round_aux_correct [lemma, in Flocq.Appli.Fappli_IEEE]
binary_overflow [definition, in Flocq.Appli.Fappli_IEEE]
binary_round_correct [lemma, in Flocq.Appli.Fappli_IEEE]
Binary_Bits.emin [variable, in Flocq.Appli.Fappli_IEEE_bits]
binary_float_of_bits [definition, in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.Hprec [variable, in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.Hmw [variable, in Flocq.Appli.Fappli_IEEE_bits]
binary_normalize_correct [lemma, in Flocq.Appli.Fappli_IEEE]
binary_float [inductive, in Flocq.Appli.Fappli_IEEE]
binary_float_of_bits_aux_correct [lemma, in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.Hm_gt_0 [variable, in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.mw [variable, in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.He_gt_0 [variable, in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.binary_float [variable, in Flocq.Appli.Fappli_IEEE_bits]
Binary.emax [variable, in Flocq.Appli.Fappli_IEEE]
Binary.emin [variable, in Flocq.Appli.Fappli_IEEE]
Binary.fexp [variable, in Flocq.Appli.Fappli_IEEE]
Binary.Hmax [variable, in Flocq.Appli.Fappli_IEEE]
Binary.prec [variable, in Flocq.Appli.Fappli_IEEE]
binary32 [definition, in Flocq.Appli.Fappli_IEEE_bits]
binary64 [definition, in Flocq.Appli.Fappli_IEEE_bits]
bits_of_binary_float_of_bits [lemma, in Flocq.Appli.Fappli_IEEE_bits]
bits_of_binary_float [definition, in Flocq.Appli.Fappli_IEEE_bits]
bits_of_b32 [definition, in Flocq.Appli.Fappli_IEEE_bits]
bits_of_b64 [definition, in Flocq.Appli.Fappli_IEEE_bits]
Bminus [definition, in Flocq.Appli.Fappli_IEEE]
Bminus_correct [lemma, in Flocq.Appli.Fappli_IEEE]
Bmult [definition, in Flocq.Appli.Fappli_IEEE]
Bmult_correct [lemma, in Flocq.Appli.Fappli_IEEE]
Bmult_FF [definition, in Flocq.Appli.Fappli_IEEE]
Bmult_correct_aux [lemma, in Flocq.Appli.Fappli_IEEE]
Bool [section, in Flocq.Core.Fcore_Raux]
Bopp [definition, in Flocq.Appli.Fappli_IEEE]
Bopp_involutive [lemma, in Flocq.Appli.Fappli_IEEE]
bounded [definition, in Flocq.Appli.Fappli_IEEE]
bounded_canonic_lt_emax [lemma, in Flocq.Appli.Fappli_IEEE]
bounded_lt_emax [lemma, in Flocq.Appli.Fappli_IEEE]
Bplus [definition, in Flocq.Appli.Fappli_IEEE]
Bplus_correct [lemma, in Flocq.Appli.Fappli_IEEE]
bpow [abbreviation, in Flocq.Prop.Fprop_div_sqrt_error]
bpow [abbreviation, in Flocq.Prop.Fprop_plus_error]
bpow [abbreviation, in Flocq.Core.Fcore_rnd_ne]
bpow [abbreviation, in Flocq.Prop.Fprop_relative]
bpow [abbreviation, in Flocq.Prop.Fprop_mult_error]
bpow [abbreviation, in Flocq.Core.Fcore_ulp]
bpow [abbreviation, in Flocq.Core.Fcore_float_prop]
bpow [abbreviation, in Flocq.Core.Fcore_FLT]
bpow [abbreviation, in Flocq.Calc.Fcalc_bracket]
bpow [abbreviation, in Flocq.Prop.Fprop_plus_error]
bpow [abbreviation, in Flocq.Prop.Fprop_Sterbenz]
bpow [definition, in Flocq.Core.Fcore_Raux]
bpow [abbreviation, in Flocq.Core.Fcore_FLX]
bpow [abbreviation, in Flocq.Calc.Fcalc_ops]
bpow [abbreviation, in Flocq.Core.Fcore_generic_fmt]
bpow [abbreviation, in Flocq.Core.Fcore_FIX]
bpow [abbreviation, in Flocq.Calc.Fcalc_sqrt]
bpow [abbreviation, in Flocq.Core.Fcore_FTZ]
bpow [abbreviation, in Flocq.Calc.Fcalc_round]
bpow [abbreviation, in Flocq.Prop.Fprop_mult_error]
bpow [abbreviation, in Flocq.Calc.Fcalc_div]
bpow [abbreviation, in Flocq.Calc.Fcalc_digits]
bpow_lt_bpow [lemma, in Flocq.Core.Fcore_Raux]
bpow_1 [lemma, in Flocq.Core.Fcore_Raux]
bpow_unique [lemma, in Flocq.Core.Fcore_Raux]
bpow_plus [lemma, in Flocq.Core.Fcore_Raux]
bpow_gt_0 [lemma, in Flocq.Core.Fcore_Raux]
bpow_plus1 [lemma, in Flocq.Core.Fcore_Raux]
bpow_ge_0 [lemma, in Flocq.Core.Fcore_Raux]
bpow_le_F2R_m1 [lemma, in Flocq.Core.Fcore_float_prop]
bpow_lt [lemma, in Flocq.Core.Fcore_Raux]
bpow_inj [lemma, in Flocq.Core.Fcore_Raux]
bpow_opp [lemma, in Flocq.Core.Fcore_Raux]
bpow_le [lemma, in Flocq.Core.Fcore_Raux]
bpow_le_F2R [lemma, in Flocq.Core.Fcore_float_prop]
bpow_exp [lemma, in Flocq.Core.Fcore_Raux]
bpow_powerRZ [lemma, in Flocq.Core.Fcore_Raux]
Bsign [definition, in Flocq.Appli.Fappli_IEEE]
Bsign_FF2B [lemma, in Flocq.Appli.Fappli_IEEE]
Bsqrt [definition, in Flocq.Appli.Fappli_IEEE]
Bsqrt_correct_aux [lemma, in Flocq.Appli.Fappli_IEEE]
Bsqrt_correct [lemma, in Flocq.Appli.Fappli_IEEE]
B2FF [definition, in Flocq.Appli.Fappli_IEEE]
B2FF_Bmult [lemma, in Flocq.Appli.Fappli_IEEE]
B2FF_FF2B [lemma, in Flocq.Appli.Fappli_IEEE]
B2FF_inj [lemma, in Flocq.Appli.Fappli_IEEE]
B2R [definition, in Flocq.Appli.Fappli_IEEE]
B2R_inj [lemma, in Flocq.Appli.Fappli_IEEE]
B2R_Bopp [lemma, in Flocq.Appli.Fappli_IEEE]
B2R_FF2B [lemma, in Flocq.Appli.Fappli_IEEE]
B32_Bits.Hprec [variable, in Flocq.Appli.Fappli_IEEE_bits]
b32_mult [definition, in Flocq.Appli.Fappli_IEEE_bits]
b32_opp [definition, in Flocq.Appli.Fappli_IEEE_bits]
B32_Bits.Hprec_emax [variable, in Flocq.Appli.Fappli_IEEE_bits]
b32_div [definition, in Flocq.Appli.Fappli_IEEE_bits]
b32_plus [definition, in Flocq.Appli.Fappli_IEEE_bits]
b32_of_bits [definition, in Flocq.Appli.Fappli_IEEE_bits]
B32_Bits [section, in Flocq.Appli.Fappli_IEEE_bits]
b32_sqrt [definition, in Flocq.Appli.Fappli_IEEE_bits]
b32_minus [definition, in Flocq.Appli.Fappli_IEEE_bits]
B64_Bits.Hprec [variable, in Flocq.Appli.Fappli_IEEE_bits]
b64_div [definition, in Flocq.Appli.Fappli_IEEE_bits]
B64_Bits [section, in Flocq.Appli.Fappli_IEEE_bits]
b64_plus [definition, in Flocq.Appli.Fappli_IEEE_bits]
b64_of_bits [definition, in Flocq.Appli.Fappli_IEEE_bits]
b64_opp [definition, in Flocq.Appli.Fappli_IEEE_bits]
b64_sqrt [definition, in Flocq.Appli.Fappli_IEEE_bits]
b64_minus [definition, in Flocq.Appli.Fappli_IEEE_bits]
b64_mult [definition, in Flocq.Appli.Fappli_IEEE_bits]
B64_Bits.Hprec_emax [variable, in Flocq.Appli.Fappli_IEEE_bits]
B754_nan [constructor, in Flocq.Appli.Fappli_IEEE]
B754_infinity [constructor, in Flocq.Appli.Fappli_IEEE]
B754_finite [constructor, in Flocq.Appli.Fappli_IEEE]
B754_zero [constructor, in Flocq.Appli.Fappli_IEEE]


C

canonic [abbreviation, in Flocq.Core.Fcore_rnd_ne]
canonic [definition, in Flocq.Core.Fcore_generic_fmt]
canonic_unicity [lemma, in Flocq.Core.Fcore_generic_fmt]
canonic_exp_round_ge [lemma, in Flocq.Core.Fcore_generic_fmt]
canonic_exp_fexp_pos [lemma, in Flocq.Core.Fcore_generic_fmt]
canonic_exp_FLT_FIX [lemma, in Flocq.Core.Fcore_FLT]
canonic_canonic_mantissa [lemma, in Flocq.Appli.Fappli_IEEE]
canonic_exp_FLT_FLX [lemma, in Flocq.Core.Fcore_FLT]
canonic_exp [definition, in Flocq.Core.Fcore_generic_fmt]
canonic_exp_DN [lemma, in Flocq.Core.Fcore_generic_fmt]
canonic_exp_fexp [lemma, in Flocq.Core.Fcore_generic_fmt]
canonic_opp [lemma, in Flocq.Core.Fcore_generic_fmt]
canonic_exp_opp [lemma, in Flocq.Core.Fcore_generic_fmt]
canonic_mantissa [definition, in Flocq.Appli.Fappli_IEEE]
canonic_exp_abs [lemma, in Flocq.Core.Fcore_generic_fmt]
cexp [abbreviation, in Flocq.Prop.Fprop_mult_error]
cexp [abbreviation, in Flocq.Prop.Fprop_mult_error]
cexp [abbreviation, in Flocq.Prop.Fprop_div_sqrt_error]
choice_mode [definition, in Flocq.Appli.Fappli_IEEE]
cond_Ropp_Rlt_bool [lemma, in Flocq.Core.Fcore_Raux]
cond_Ropp [definition, in Flocq.Core.Fcore_Raux]
cond_Zopp [definition, in Flocq.Core.Fcore_Raux]
cond_Zopp_Zlt_bool [lemma, in Flocq.Core.Fcore_Raux]
cond_incr [definition, in Flocq.Calc.Fcalc_round]
cond_opp [section, in Flocq.Core.Fcore_Raux]


D

Def [section, in Flocq.Core.Fcore_defs]
Def.beta [variable, in Flocq.Core.Fcore_defs]
digits2_Pnat [definition, in Flocq.Core.Fcore_digits]
digits2_Pnat_correct [lemma, in Flocq.Core.Fcore_digits]
Div_Mod [section, in Flocq.Core.Fcore_Zaux]
div_error_FLX [lemma, in Flocq.Prop.Fprop_div_sqrt_error]
DN_UP_parity_aux [lemma, in Flocq.Core.Fcore_rnd_ne]
DN_UP_parity_prop [definition, in Flocq.Core.Fcore_rnd_ne]
DN_UP_parity_generic [lemma, in Flocq.Core.Fcore_rnd_ne]
DN_UP_parity_generic_pos [lemma, in Flocq.Core.Fcore_rnd_ne]
DN_UP_parity_pos_prop [definition, in Flocq.Core.Fcore_rnd_ne]


E

eqbool_dep [definition, in Flocq.Core.Fcore_Zaux]
eqbool_irrelevance [lemma, in Flocq.Core.Fcore_Zaux]
eqb_false [lemma, in Flocq.Core.Fcore_Raux]
eqb_sym [lemma, in Flocq.Core.Fcore_Raux]
eqb_true [lemma, in Flocq.Core.Fcore_Raux]
eq_Z2R [lemma, in Flocq.Core.Fcore_Raux]
error_N_FLT_aux [lemma, in Flocq.Prop.Fprop_relative]
Even_Odd [section, in Flocq.Core.Fcore_Zaux]
exists_NE_FLX [instance, in Flocq.Core.Fcore_FLX]
Exists_NE [record, in Flocq.Core.Fcore_rnd_ne]
Exists_NE [inductive, in Flocq.Core.Fcore_rnd_ne]
exists_NE_FLT [instance, in Flocq.Core.Fcore_FLT]
exists_NE [projection, in Flocq.Core.Fcore_rnd_ne]
exists_NE [constructor, in Flocq.Core.Fcore_rnd_ne]
exp_not_FTZ [projection, in Flocq.Core.Fcore_generic_fmt]
exp_not_FTZ [constructor, in Flocq.Core.Fcore_generic_fmt]
exp_le [lemma, in Flocq.Core.Fcore_Raux]
Exp_not_FTZ [record, in Flocq.Core.Fcore_generic_fmt]
Exp_not_FTZ [inductive, in Flocq.Core.Fcore_generic_fmt]
ex_Fexp_canonic [lemma, in Flocq.Prop.Fprop_div_sqrt_error]


F

F [abbreviation, in Flocq.Core.Fcore_ulp]
Fabs [definition, in Flocq.Calc.Fcalc_ops]
Falign [definition, in Flocq.Calc.Fcalc_ops]
Falign_spec [lemma, in Flocq.Calc.Fcalc_ops]
Falign_spec_exp [lemma, in Flocq.Calc.Fcalc_ops]
Fappli_IEEE_bits [library]
Fappli_IEEE [library]
Fcalc_digits.beta [variable, in Flocq.Calc.Fcalc_digits]
Fcalc_bracket.u [variable, in Flocq.Calc.Fcalc_bracket]
Fcalc_round.Fcalc_round_fexp.round_dir_sign.choice [variable, in Flocq.Calc.Fcalc_round]
Fcalc_bracket.Fcalc_bracket_any [section, in Flocq.Calc.Fcalc_bracket]
Fcalc_round.Fcalc_round_fexp.round_dir [section, in Flocq.Calc.Fcalc_round]
Fcalc_bracket_scale [section, in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket_step.Hnb_steps [variable, in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket_step.start [variable, in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket_step.step [variable, in Flocq.Calc.Fcalc_bracket]
Fcalc_round.emin [variable, in Flocq.Calc.Fcalc_round]
Fcalc_bracket [section, in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket_step.Hstep [variable, in Flocq.Calc.Fcalc_bracket]
Fcalc_round.Fcalc_round_fexp.round_dir.rnd [variable, in Flocq.Calc.Fcalc_round]
Fcalc_div [section, in Flocq.Calc.Fcalc_div]
Fcalc_round.Fcalc_round_fexp.round_dir_sign.inbetween_int_valid [variable, in Flocq.Calc.Fcalc_round]
Fcalc_sqrt [section, in Flocq.Calc.Fcalc_sqrt]
Fcalc_round.Fcalc_round_fexp.round_dir.inbetween_int_valid [variable, in Flocq.Calc.Fcalc_round]
Fcalc_bracket_step [section, in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket.x [variable, in Flocq.Calc.Fcalc_bracket]
Fcalc_round.Fcalc_round_fexp.round_dir_sign.rnd [variable, in Flocq.Calc.Fcalc_round]
Fcalc_round.Fcalc_round_fexp [section, in Flocq.Calc.Fcalc_round]
Fcalc_round.Fcalc_round_fexp.round_dir_sign [section, in Flocq.Calc.Fcalc_round]
Fcalc_round [section, in Flocq.Calc.Fcalc_round]
Fcalc_round.Fcalc_round_fexp.fexp [variable, in Flocq.Calc.Fcalc_round]
Fcalc_bracket_generic [section, in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket.Hdu [variable, in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket_step.nb_steps [variable, in Flocq.Calc.Fcalc_bracket]
Fcalc_div.beta [variable, in Flocq.Calc.Fcalc_div]
Fcalc_bracket.d [variable, in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket.Fcalc_bracket_any.l [variable, in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket_generic.beta [variable, in Flocq.Calc.Fcalc_bracket]
Fcalc_round.beta [variable, in Flocq.Calc.Fcalc_round]
Fcalc_sqrt.beta [variable, in Flocq.Calc.Fcalc_sqrt]
Fcalc_round.Fcalc_round_fexp.round_dir.choice [variable, in Flocq.Calc.Fcalc_round]
Fcalc_digits [section, in Flocq.Calc.Fcalc_digits]
Fcalc_div [library]
Fcalc_bracket [library]
Fcalc_round [library]
Fcalc_ops [library]
Fcalc_sqrt [library]
Fcalc_digits [library]
Fcore [library]
Fcore_ulp [section, in Flocq.Core.Fcore_ulp]
Fcore_rnd_NE [section, in Flocq.Core.Fcore_rnd_ne]
Fcore_rnd_NE.beta [variable, in Flocq.Core.Fcore_rnd_ne]
Fcore_ulp.fexp [variable, in Flocq.Core.Fcore_ulp]
Fcore_digits.digits_aux.Hp [variable, in Flocq.Core.Fcore_digits]
Fcore_rnd_NE.fexp [variable, in Flocq.Core.Fcore_rnd_ne]
Fcore_digits.digits_aux [section, in Flocq.Core.Fcore_digits]
Fcore_ulp.beta [variable, in Flocq.Core.Fcore_ulp]
Fcore_digits [section, in Flocq.Core.Fcore_digits]
Fcore_digits.beta [variable, in Flocq.Core.Fcore_digits]
Fcore_digits.digits_aux.p [variable, in Flocq.Core.Fcore_digits]
Fcore_FIX [library]
Fcore_ulp [library]
Fcore_rnd [library]
Fcore_Raux [library]
Fcore_FTZ [library]
Fcore_generic_fmt [library]
Fcore_float_prop [library]
Fcore_FLT [library]
Fcore_FLX [library]
Fcore_Zaux [library]
Fcore_defs [library]
Fcore_digits [library]
Fcore_rnd_ne [library]
Fdiv_core_correct [lemma, in Flocq.Calc.Fcalc_div]
Fdiv_core_binary [definition, in Flocq.Appli.Fappli_IEEE]
Fdiv_core [definition, in Flocq.Calc.Fcalc_div]
Fexp [projection, in Flocq.Core.Fcore_defs]
Fexp_Fplus [lemma, in Flocq.Calc.Fcalc_ops]
fexp_monotone [instance, in Flocq.Appli.Fappli_IEEE]
fexp_correct [instance, in Flocq.Appli.Fappli_IEEE]
FF2B [definition, in Flocq.Appli.Fappli_IEEE]
FF2B_B2FF_valid [lemma, in Flocq.Appli.Fappli_IEEE]
FF2B_B2FF [lemma, in Flocq.Appli.Fappli_IEEE]
FF2R [definition, in Flocq.Appli.Fappli_IEEE]
FF2R_B2FF [lemma, in Flocq.Appli.Fappli_IEEE]
FIX_format_generic [lemma, in Flocq.Core.Fcore_FIX]
FIX_exp [definition, in Flocq.Core.Fcore_FIX]
FIX_exp_monotone [instance, in Flocq.Core.Fcore_FIX]
FIX_format_satisfies_any [lemma, in Flocq.Core.Fcore_FIX]
FIX_format_FLX [lemma, in Flocq.Core.Fcore_FLX]
FIX_exp_valid [instance, in Flocq.Core.Fcore_FIX]
FIX_format [definition, in Flocq.Core.Fcore_FIX]
float [record, in Flocq.Core.Fcore_defs]
Float [constructor, in Flocq.Core.Fcore_defs]
float_distribution_pos [lemma, in Flocq.Core.Fcore_float_prop]
Float_ops.beta [variable, in Flocq.Calc.Fcalc_ops]
Float_prop [section, in Flocq.Core.Fcore_float_prop]
Float_ops [section, in Flocq.Calc.Fcalc_ops]
Float_prop.beta [variable, in Flocq.Core.Fcore_float_prop]
Flocq_version [definition, in Flocq.Flocq_version]
Flocq_version [library]
Floor_Ceil [section, in Flocq.Core.Fcore_Raux]
FLT_format_generic [lemma, in Flocq.Core.Fcore_FLT]
FLT_format_satisfies_any [lemma, in Flocq.Core.Fcore_FLT]
FLT_exp_valid [instance, in Flocq.Core.Fcore_FLT]
FLT_exp [definition, in Flocq.Core.Fcore_FLT]
FLT_format [definition, in Flocq.Core.Fcore_FLT]
FLT_exp_monotone [instance, in Flocq.Core.Fcore_FLT]
FLXN_format [definition, in Flocq.Core.Fcore_FLX]
FLXN_format_generic [lemma, in Flocq.Core.Fcore_FLX]
FLXN_format_satisfies_any [lemma, in Flocq.Core.Fcore_FLX]
FLXN_format_FTZ [lemma, in Flocq.Core.Fcore_FTZ]
FLX_format_FIX [lemma, in Flocq.Core.Fcore_FLX]
FLX_exp_monotone [instance, in Flocq.Core.Fcore_FLX]
FLX_exp_valid [instance, in Flocq.Core.Fcore_FLX]
FLX_format_satisfies_any [lemma, in Flocq.Core.Fcore_FLX]
FLX_format_generic [lemma, in Flocq.Core.Fcore_FLX]
FLX_exp [definition, in Flocq.Core.Fcore_FLX]
FLX_format [definition, in Flocq.Core.Fcore_FLX]
Fminus [definition, in Flocq.Calc.Fcalc_ops]
Fminus_same_exp [lemma, in Flocq.Calc.Fcalc_ops]
Fmult [definition, in Flocq.Calc.Fcalc_ops]
Fnum [projection, in Flocq.Core.Fcore_defs]
Fopp [definition, in Flocq.Calc.Fcalc_ops]
format [abbreviation, in Flocq.Prop.Fprop_plus_error]
format [abbreviation, in Flocq.Calc.Fcalc_round]
format [abbreviation, in Flocq.Prop.Fprop_Sterbenz]
format [abbreviation, in Flocq.Prop.Fprop_plus_error]
format [abbreviation, in Flocq.Core.Fcore_rnd_ne]
format [abbreviation, in Flocq.Prop.Fprop_mult_error]
format [abbreviation, in Flocq.Prop.Fprop_div_sqrt_error]
format [abbreviation, in Flocq.Prop.Fprop_mult_error]
Fplus [definition, in Flocq.Calc.Fcalc_ops]
Fplus_same_exp [lemma, in Flocq.Calc.Fcalc_ops]
Fprop_relative.Fprop_relative_FLT.prec [variable, in Flocq.Prop.Fprop_relative]
Fprop_plus_zero.round_plus_eq_zero_aux.rnd [variable, in Flocq.Prop.Fprop_plus_error]
Fprop_mult_error.rnd [variable, in Flocq.Prop.Fprop_mult_error]
Fprop_relative.Fprop_relative_FLT.rnd [variable, in Flocq.Prop.Fprop_relative]
Fprop_relative.beta [variable, in Flocq.Prop.Fprop_relative]
Fprop_mult_error_FLT.rnd [variable, in Flocq.Prop.Fprop_mult_error]
Fprop_mult_error_FLT.Hpemin [variable, in Flocq.Prop.Fprop_mult_error]
Fprop_plus_zero [section, in Flocq.Prop.Fprop_plus_error]
Fprop_mult_error_FLT.emin [variable, in Flocq.Prop.Fprop_mult_error]
Fprop_relative.Fprop_relative_FLT [section, in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_generic.p [variable, in Flocq.Prop.Fprop_relative]
Fprop_mult_error_FLT.prec [variable, in Flocq.Prop.Fprop_mult_error]
Fprop_mult_error_FLT.beta [variable, in Flocq.Prop.Fprop_mult_error]
Fprop_relative.Fprop_relative_FLT.emin [variable, in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_FLX.choice [variable, in Flocq.Prop.Fprop_relative]
Fprop_divsqrt_error.prec [variable, in Flocq.Prop.Fprop_div_sqrt_error]
Fprop_divsqrt_error.Hp1 [variable, in Flocq.Prop.Fprop_div_sqrt_error]
Fprop_relative.Fprop_relative_FLX [section, in Flocq.Prop.Fprop_relative]
Fprop_mult_error.beta [variable, in Flocq.Prop.Fprop_mult_error]
Fprop_Sterbenz.fexp [variable, in Flocq.Prop.Fprop_Sterbenz]
Fprop_mult_error [section, in Flocq.Prop.Fprop_mult_error]
Fprop_plus_zero.fexp [variable, in Flocq.Prop.Fprop_plus_error]
Fprop_plus_error.fexp [variable, in Flocq.Prop.Fprop_plus_error]
Fprop_relative.Fprop_relative_generic.emin [variable, in Flocq.Prop.Fprop_relative]
Fprop_plus_zero.beta [variable, in Flocq.Prop.Fprop_plus_error]
Fprop_Sterbenz [section, in Flocq.Prop.Fprop_Sterbenz]
Fprop_plus_error.choice [variable, in Flocq.Prop.Fprop_plus_error]
Fprop_plus_error.beta [variable, in Flocq.Prop.Fprop_plus_error]
Fprop_relative.Fprop_relative_generic.Hmin [variable, in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_generic [section, in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_generic.relative_error_conversion [section, in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_generic.rnd [variable, in Flocq.Prop.Fprop_relative]
Fprop_plus_zero.round_plus_eq_zero_aux [section, in Flocq.Prop.Fprop_plus_error]
Fprop_plus_zero.rnd [variable, in Flocq.Prop.Fprop_plus_error]
Fprop_relative.Fprop_relative_FLX.Hp [variable, in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_FLT.Hp [variable, in Flocq.Prop.Fprop_relative]
Fprop_plus_error.round_repr_same_exp.rnd [variable, in Flocq.Prop.Fprop_plus_error]
Fprop_Sterbenz.beta [variable, in Flocq.Prop.Fprop_Sterbenz]
Fprop_divsqrt_error.beta [variable, in Flocq.Prop.Fprop_div_sqrt_error]
Fprop_plus_error [section, in Flocq.Prop.Fprop_plus_error]
Fprop_relative.Fprop_relative_generic.fexp [variable, in Flocq.Prop.Fprop_relative]
Fprop_divsqrt_error.choice [variable, in Flocq.Prop.Fprop_div_sqrt_error]
Fprop_relative.Fprop_relative_generic.choice [variable, in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_FLX.rnd [variable, in Flocq.Prop.Fprop_relative]
Fprop_relative [section, in Flocq.Prop.Fprop_relative]
Fprop_plus_error.round_repr_same_exp [section, in Flocq.Prop.Fprop_plus_error]
Fprop_relative.Fprop_relative_FLT.choice [variable, in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_generic.relative_error_conversion.rnd [variable, in Flocq.Prop.Fprop_relative]
Fprop_divsqrt_error [section, in Flocq.Prop.Fprop_div_sqrt_error]
Fprop_mult_error.prec [variable, in Flocq.Prop.Fprop_mult_error]
Fprop_mult_error_FLT [section, in Flocq.Prop.Fprop_mult_error]
Fprop_relative.Fprop_relative_FLX.prec [variable, in Flocq.Prop.Fprop_relative]
Fprop_Sterbenz [library]
Fprop_div_sqrt_error [library]
Fprop_relative [library]
Fprop_mult_error [library]
Fprop_plus_error [library]
Fsqrt_core [definition, in Flocq.Calc.Fcalc_sqrt]
Fsqrt_core_binary [definition, in Flocq.Appli.Fappli_IEEE]
Fsqrt_core_correct [lemma, in Flocq.Calc.Fcalc_sqrt]
FTZ_format [definition, in Flocq.Core.Fcore_FTZ]
FTZ_exp [definition, in Flocq.Core.Fcore_FTZ]
FTZ_exp_valid [instance, in Flocq.Core.Fcore_FTZ]
FTZ_format_FLXN [lemma, in Flocq.Core.Fcore_FTZ]
FTZ_format_generic [lemma, in Flocq.Core.Fcore_FTZ]
FTZ_format_satisfies_any [lemma, in Flocq.Core.Fcore_FTZ]
full_float [inductive, in Flocq.Appli.Fappli_IEEE]
F2R [definition, in Flocq.Core.Fcore_defs]
F2R_plus [lemma, in Flocq.Calc.Fcalc_ops]
F2R_gt_0_compat [lemma, in Flocq.Core.Fcore_float_prop]
F2R_lt_0_reg [lemma, in Flocq.Core.Fcore_float_prop]
F2R_prec_normalize [lemma, in Flocq.Core.Fcore_float_prop]
F2R_mult [lemma, in Flocq.Calc.Fcalc_ops]
F2R_0 [lemma, in Flocq.Core.Fcore_float_prop]
F2R_cond_Zopp [lemma, in Flocq.Core.Fcore_float_prop]
F2R_change_exp [lemma, in Flocq.Core.Fcore_float_prop]
F2R_lt_bpow [lemma, in Flocq.Core.Fcore_float_prop]
F2R_gt_0_reg [lemma, in Flocq.Core.Fcore_float_prop]
F2R_bpow [lemma, in Flocq.Core.Fcore_float_prop]
F2R_lt_0_compat [lemma, in Flocq.Core.Fcore_float_prop]
F2R_abs [lemma, in Flocq.Calc.Fcalc_ops]
F2R_eq_0_reg [lemma, in Flocq.Core.Fcore_float_prop]
F2R_le_0_compat [lemma, in Flocq.Core.Fcore_float_prop]
F2R_le_compat [lemma, in Flocq.Core.Fcore_float_prop]
F2R_Zabs [lemma, in Flocq.Core.Fcore_float_prop]
F2R_lt_reg [lemma, in Flocq.Core.Fcore_float_prop]
F2R_Zopp [lemma, in Flocq.Core.Fcore_float_prop]
F2R_eq_reg [lemma, in Flocq.Core.Fcore_float_prop]
F2R_minus [lemma, in Flocq.Calc.Fcalc_ops]
F2R_p1_le_bpow [lemma, in Flocq.Core.Fcore_float_prop]
F2R_ge_0_reg [lemma, in Flocq.Core.Fcore_float_prop]
F2R_le_0_reg [lemma, in Flocq.Core.Fcore_float_prop]
F2R_le_reg [lemma, in Flocq.Core.Fcore_float_prop]
F2R_ge_0_compat [lemma, in Flocq.Core.Fcore_float_prop]
F2R_lt_compat [lemma, in Flocq.Core.Fcore_float_prop]
F2R_eq_compat [lemma, in Flocq.Core.Fcore_float_prop]
F2R_opp [lemma, in Flocq.Calc.Fcalc_ops]
F754_zero [constructor, in Flocq.Appli.Fappli_IEEE]
F754_finite [constructor, in Flocq.Appli.Fappli_IEEE]
F754_infinity [constructor, in Flocq.Appli.Fappli_IEEE]
F754_nan [constructor, in Flocq.Appli.Fappli_IEEE]


G

Generic [section, in Flocq.Core.Fcore_generic_fmt]
generic_format_FLT_FIX [lemma, in Flocq.Core.Fcore_FLT]
generic_format_plus_weak [lemma, in Flocq.Prop.Fprop_Sterbenz]
generic_format_truncate [lemma, in Flocq.Calc.Fcalc_round]
generic_format_plus_prec [lemma, in Flocq.Prop.Fprop_div_sqrt_error]
generic_format_F2R [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_B2R [lemma, in Flocq.Appli.Fappli_IEEE]
generic_format_EM [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_abs_inv [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_pred [lemma, in Flocq.Core.Fcore_ulp]
generic_format_succ [lemma, in Flocq.Core.Fcore_ulp]
generic_format_pred_1 [lemma, in Flocq.Core.Fcore_ulp]
generic_inclusion_ge [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_inclusion_ln_beta [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_0 [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_FIX_FLT [lemma, in Flocq.Core.Fcore_FLT]
generic_format_opp [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_inclusion_le_ge [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_FLT [lemma, in Flocq.Core.Fcore_FLT]
generic_format_ge_bpow [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format [definition, in Flocq.Core.Fcore_generic_fmt]
generic_format_satisfies_any [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_FIX [lemma, in Flocq.Core.Fcore_FIX]
generic_format_FLX [lemma, in Flocq.Core.Fcore_FLX]
generic_format_discrete [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_FLXN [lemma, in Flocq.Core.Fcore_FLX]
generic_inclusion_lt_ge [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_FLX_FLT [lemma, in Flocq.Core.Fcore_FLT]
generic_inclusion [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_inclusion_le [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_abs [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_N_pt_DN_or_UP [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_plus [lemma, in Flocq.Prop.Fprop_Sterbenz]
generic_format_FTZ [lemma, in Flocq.Core.Fcore_FTZ]
generic_format_bpow_inv [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_bpow' [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_FLT_FLX [lemma, in Flocq.Core.Fcore_FLT]
generic_format_pred_2 [lemma, in Flocq.Core.Fcore_ulp]
generic_format_round_pos [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_bpow [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_canonic [lemma, in Flocq.Core.Fcore_generic_fmt]
generic_format_round [lemma, in Flocq.Core.Fcore_generic_fmt]
Generic.beta [variable, in Flocq.Core.Fcore_generic_fmt]
Generic.Format [section, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.Fcore_generic_round_pos.rnd [variable, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.Fcore_generic_round_pos [section, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.fexp [variable, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.monotone [section, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.monotone_abs [section, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.monotone_exp.rnd [variable, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.monotone_exp [section, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.monotone_abs.rnd [variable, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.monotone.rnd [variable, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.not_FTZ [section, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.rndNA [section, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.rndN_opp [section, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.round_large.rnd [variable, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.round_large [section, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.Znearest [section, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.Znearest.choice [variable, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.Zround_opp.rnd [variable, in Flocq.Core.Fcore_generic_fmt]
Generic.Format.Zround_opp [section, in Flocq.Core.Fcore_generic_fmt]
Generic.Inclusion [section, in Flocq.Core.Fcore_generic_fmt]
Generic.Inclusion.fexp1 [variable, in Flocq.Core.Fcore_generic_fmt]
Generic.Inclusion.fexp2 [variable, in Flocq.Core.Fcore_generic_fmt]


I

inbetween [inductive, in Flocq.Calc.Fcalc_bracket]
inbetween_float_round [lemma, in Flocq.Calc.Fcalc_round]
inbetween_spec [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_step_Lo_Mi_Eq_odd [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_distance_inexact_abs [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_step_any_Mi_odd [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_float_unique [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_int_UP [lemma, in Flocq.Calc.Fcalc_round]
inbetween_float_new_location [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_step_Hi_Mi_even [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_mult_compat [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_float_UP [lemma, in Flocq.Calc.Fcalc_round]
inbetween_float_UP_sign [lemma, in Flocq.Calc.Fcalc_round]
inbetween_distance_inexact [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_step_Hi [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_float_ZR [lemma, in Flocq.Calc.Fcalc_round]
inbetween_int_NE [lemma, in Flocq.Calc.Fcalc_round]
inbetween_mult_aux [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_float_round_sign [lemma, in Flocq.Calc.Fcalc_round]
inbetween_float_ex [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_bounds [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_int [definition, in Flocq.Calc.Fcalc_bracket]
inbetween_Inexact [constructor, in Flocq.Calc.Fcalc_bracket]
inbetween_int_ZR [lemma, in Flocq.Calc.Fcalc_round]
inbetween_float_DN_sign [lemma, in Flocq.Calc.Fcalc_round]
inbetween_shr_1 [lemma, in Flocq.Appli.Fappli_IEEE]
inbetween_int_ZR_sign [lemma, in Flocq.Calc.Fcalc_round]
inbetween_Exact [constructor, in Flocq.Calc.Fcalc_bracket]
inbetween_float_ZR_sign [lemma, in Flocq.Calc.Fcalc_round]
inbetween_float [definition, in Flocq.Calc.Fcalc_bracket]
inbetween_int_N_sign [lemma, in Flocq.Calc.Fcalc_round]
inbetween_step_Mi_Mi_even [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_bounds_not_Eq [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_unique [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_float_NA [lemma, in Flocq.Calc.Fcalc_round]
inbetween_float_NE_sign [lemma, in Flocq.Calc.Fcalc_round]
inbetween_mult_reg [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_int_N [lemma, in Flocq.Calc.Fcalc_round]
inbetween_int_NA_sign [lemma, in Flocq.Calc.Fcalc_round]
inbetween_step_not_Eq [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_shr [lemma, in Flocq.Appli.Fappli_IEEE]
inbetween_int_DN [lemma, in Flocq.Calc.Fcalc_round]
inbetween_float_bounds [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_float_new_location_single [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_float_NE [lemma, in Flocq.Calc.Fcalc_round]
inbetween_float_DN [lemma, in Flocq.Calc.Fcalc_round]
inbetween_int_UP_sign [lemma, in Flocq.Calc.Fcalc_round]
inbetween_step_Lo [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_int_NA [lemma, in Flocq.Calc.Fcalc_round]
inbetween_loc [definition, in Flocq.Calc.Fcalc_bracket]
inbetween_ex [lemma, in Flocq.Calc.Fcalc_bracket]
inbetween_int_NE_sign [lemma, in Flocq.Calc.Fcalc_round]
inbetween_int_DN_sign [lemma, in Flocq.Calc.Fcalc_round]
inbetween_step_Lo_not_Eq [lemma, in Flocq.Calc.Fcalc_bracket]
is_finite [definition, in Flocq.Appli.Fappli_IEEE]
is_finite_FF [definition, in Flocq.Appli.Fappli_IEEE]
is_finite_FF_B2FF [lemma, in Flocq.Appli.Fappli_IEEE]
is_finite_FF2B [lemma, in Flocq.Appli.Fappli_IEEE]
is_finite_Bopp [lemma, in Flocq.Appli.Fappli_IEEE]
is_finite_strict [definition, in Flocq.Appli.Fappli_IEEE]


J

join_split_bits [lemma, in Flocq.Appli.Fappli_IEEE_bits]
join_bits [definition, in Flocq.Appli.Fappli_IEEE_bits]


L

le_pred_lt_aux [lemma, in Flocq.Core.Fcore_ulp]
le_pred_lt [lemma, in Flocq.Core.Fcore_ulp]
le_Z2R [lemma, in Flocq.Core.Fcore_Raux]
le_bpow [lemma, in Flocq.Core.Fcore_Raux]
le_lt_Z2R [lemma, in Flocq.Core.Fcore_Raux]
ln_beta_gt_bpow [lemma, in Flocq.Core.Fcore_Raux]
ln_beta_opp [lemma, in Flocq.Core.Fcore_Raux]
ln_beta_val [projection, in Flocq.Core.Fcore_Raux]
ln_beta [definition, in Flocq.Core.Fcore_Raux]
ln_beta_abs [lemma, in Flocq.Core.Fcore_Raux]
ln_beta_F2R [lemma, in Flocq.Core.Fcore_float_prop]
ln_beta_prop [record, in Flocq.Core.Fcore_Raux]
ln_beta_gt_Zpower [lemma, in Flocq.Core.Fcore_Raux]
ln_beta_F2R_Zdigits [lemma, in Flocq.Calc.Fcalc_digits]
ln_beta_le_abs [lemma, in Flocq.Core.Fcore_Raux]
ln_beta_le [lemma, in Flocq.Core.Fcore_Raux]
ln_beta_F2R_bounds [lemma, in Flocq.Core.Fcore_float_prop]
ln_beta_bpow [lemma, in Flocq.Core.Fcore_Raux]
ln_beta_unique [lemma, in Flocq.Core.Fcore_Raux]
ln_beta_le_Zpower [lemma, in Flocq.Core.Fcore_Raux]
ln_beta_le_bpow [lemma, in Flocq.Core.Fcore_Raux]
ln_beta_succ [lemma, in Flocq.Core.Fcore_ulp]
location [inductive, in Flocq.Calc.Fcalc_bracket]
loc_Inexact [constructor, in Flocq.Calc.Fcalc_bracket]
loc_of_shr_record_of_loc [lemma, in Flocq.Appli.Fappli_IEEE]
loc_of_shr_record [definition, in Flocq.Appli.Fappli_IEEE]
loc_Exact [constructor, in Flocq.Calc.Fcalc_bracket]
lt_Z2R [lemma, in Flocq.Core.Fcore_Raux]
lt_bpow [lemma, in Flocq.Core.Fcore_Raux]
lt_Zdigits [lemma, in Flocq.Calc.Fcalc_digits]


M

mantissa_UP_small_pos [lemma, in Flocq.Core.Fcore_generic_fmt]
mantissa_small_pos [lemma, in Flocq.Core.Fcore_generic_fmt]
mantissa_DN_small_pos [lemma, in Flocq.Core.Fcore_generic_fmt]
match_FF2B [lemma, in Flocq.Appli.Fappli_IEEE]
middle_range [lemma, in Flocq.Calc.Fcalc_bracket]
middle_odd [lemma, in Flocq.Calc.Fcalc_bracket]
minus_IZR [lemma, in Flocq.Core.Fcore_Raux]
mode [inductive, in Flocq.Appli.Fappli_IEEE]
mode_NA [constructor, in Flocq.Appli.Fappli_IEEE]
mode_DN [constructor, in Flocq.Appli.Fappli_IEEE]
mode_UP [constructor, in Flocq.Appli.Fappli_IEEE]
mode_ZR [constructor, in Flocq.Appli.Fappli_IEEE]
mode_NE [constructor, in Flocq.Appli.Fappli_IEEE]
monotone_exp_not_FTZ [instance, in Flocq.Core.Fcore_generic_fmt]
monotone_exp [projection, in Flocq.Core.Fcore_generic_fmt]
monotone_exp [constructor, in Flocq.Core.Fcore_generic_fmt]
Monotone_exp [record, in Flocq.Core.Fcore_generic_fmt]
Monotone_exp [inductive, in Flocq.Core.Fcore_generic_fmt]
mult_error_FLX [lemma, in Flocq.Prop.Fprop_mult_error]
mult_error_FLT [lemma, in Flocq.Prop.Fprop_mult_error]
mult_error_FLX_aux [lemma, in Flocq.Prop.Fprop_mult_error]


N

negb_Rle_bool [lemma, in Flocq.Core.Fcore_Raux]
negb_Rlt_bool [lemma, in Flocq.Core.Fcore_Raux]
negb_Zlt_bool [lemma, in Flocq.Core.Fcore_Zaux]
negb_Zle_bool [lemma, in Flocq.Core.Fcore_Zaux]
neq_Z2R [lemma, in Flocq.Core.Fcore_Raux]
new_location_odd_correct [lemma, in Flocq.Calc.Fcalc_bracket]
new_location_odd [definition, in Flocq.Calc.Fcalc_bracket]
new_location_correct [lemma, in Flocq.Calc.Fcalc_bracket]
new_location_even_correct [lemma, in Flocq.Calc.Fcalc_bracket]
new_location [definition, in Flocq.Calc.Fcalc_bracket]
new_location_even [definition, in Flocq.Calc.Fcalc_bracket]
NE_prop [definition, in Flocq.Core.Fcore_rnd_ne]
NG_existence_prop [definition, in Flocq.Core.Fcore_rnd]


O

Only_DN_or_UP [lemma, in Flocq.Core.Fcore_rnd]
ordered_steps [lemma, in Flocq.Calc.Fcalc_bracket]
overflow_to_inf [definition, in Flocq.Appli.Fappli_IEEE]


P

plus_error [lemma, in Flocq.Prop.Fprop_plus_error]
plus_error_aux [lemma, in Flocq.Prop.Fprop_plus_error]
pow [section, in Flocq.Core.Fcore_Raux]
pow.r [variable, in Flocq.Core.Fcore_Raux]
prec_gt_0 [projection, in Flocq.Core.Fcore_FLX]
prec_gt_0 [constructor, in Flocq.Core.Fcore_FLX]
Prec_gt_0 [record, in Flocq.Core.Fcore_FLX]
Prec_gt_0 [inductive, in Flocq.Core.Fcore_FLX]
pred [definition, in Flocq.Core.Fcore_ulp]
pred_plus_ulp [lemma, in Flocq.Core.Fcore_ulp]
pred_ge_0 [lemma, in Flocq.Core.Fcore_ulp]
pred_ge_bpow [lemma, in Flocq.Core.Fcore_ulp]
pred_plus_ulp_1 [lemma, in Flocq.Core.Fcore_ulp]
pred_lt_id [lemma, in Flocq.Core.Fcore_ulp]
pred_plus_ulp_2 [lemma, in Flocq.Core.Fcore_ulp]
Proof_Irrelevance [section, in Flocq.Core.Fcore_Zaux]
P2R [definition, in Flocq.Core.Fcore_Raux]
P2R_INR [lemma, in Flocq.Core.Fcore_Raux]


R

Rabs_gt_inv [lemma, in Flocq.Core.Fcore_Raux]
Rabs_le [lemma, in Flocq.Core.Fcore_Raux]
Rabs_lt [lemma, in Flocq.Core.Fcore_Raux]
Rabs_ge_inv [lemma, in Flocq.Core.Fcore_Raux]
Rabs_minus_le [lemma, in Flocq.Core.Fcore_Raux]
Rabs_ge [lemma, in Flocq.Core.Fcore_Raux]
Rabs_lt_inv [lemma, in Flocq.Core.Fcore_Raux]
Rabs_gt [lemma, in Flocq.Core.Fcore_Raux]
Rabs_eq_Rabs [lemma, in Flocq.Core.Fcore_Raux]
Rabs_le_inv [lemma, in Flocq.Core.Fcore_Raux]
radix [record, in Flocq.Core.Fcore_Zaux]
radix_gt_0 [lemma, in Flocq.Core.Fcore_Zaux]
radix_val [projection, in Flocq.Core.Fcore_Zaux]
radix_val_inj [lemma, in Flocq.Core.Fcore_Zaux]
radix_prop [projection, in Flocq.Core.Fcore_Zaux]
radix_pos [lemma, in Flocq.Core.Fcore_Raux]
radix_gt_1 [lemma, in Flocq.Core.Fcore_Zaux]
radix2 [definition, in Flocq.Appli.Fappli_IEEE]
radix2 [definition, in Flocq.Calc.Fcalc_digits]
Rcompare [definition, in Flocq.Core.Fcore_Raux]
Rcompare [section, in Flocq.Core.Fcore_Raux]
Rcompare_sym [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_Z2R [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_Lt_ [constructor, in Flocq.Core.Fcore_Raux]
Rcompare_plus_r [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_Eq_ [constructor, in Flocq.Core.Fcore_Raux]
Rcompare_half_l [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_ceil_floor_mid [lemma, in Flocq.Core.Fcore_generic_fmt]
Rcompare_Lt_inv [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_floor_ceil_mid [lemma, in Flocq.Core.Fcore_generic_fmt]
Rcompare_Eq_inv [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_spec [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_Lt [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_F2R [lemma, in Flocq.Core.Fcore_float_prop]
Rcompare_not_Lt [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_Eq [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_not_Lt_inv [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_mult_l [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_Gt_ [constructor, in Flocq.Core.Fcore_Raux]
Rcompare_half_r [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_Gt_inv [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_not_Gt_inv [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_plus_l [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_Gt [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_middle [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_mult_r [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_prop [inductive, in Flocq.Core.Fcore_Raux]
Rcompare_not_Gt [lemma, in Flocq.Core.Fcore_Raux]
Rcompare_sqr [lemma, in Flocq.Core.Fcore_Raux]
relative_error_N_FLX_ex [lemma, in Flocq.Prop.Fprop_relative]
relative_error_N_F2R_emin_ex [lemma, in Flocq.Prop.Fprop_relative]
relative_error_round_F2R_emin [lemma, in Flocq.Prop.Fprop_relative]
relative_error_round [lemma, in Flocq.Prop.Fprop_relative]
relative_error_N [lemma, in Flocq.Prop.Fprop_relative]
relative_error_FLT_F2R_emin [lemma, in Flocq.Prop.Fprop_relative]
relative_error_FLT_F2R_emin_ex [lemma, in Flocq.Prop.Fprop_relative]
relative_error_N_FLT_ex [lemma, in Flocq.Prop.Fprop_relative]
relative_error_N_ex [lemma, in Flocq.Prop.Fprop_relative]
relative_error_N_F2R_emin [lemma, in Flocq.Prop.Fprop_relative]
relative_error_N_FLT [lemma, in Flocq.Prop.Fprop_relative]
relative_error_le_conversion [lemma, in Flocq.Prop.Fprop_relative]
relative_error_FLX_round [lemma, in Flocq.Prop.Fprop_relative]
relative_error_N_FLT_round_F2R_emin [lemma, in Flocq.Prop.Fprop_relative]
relative_error_N_round [lemma, in Flocq.Prop.Fprop_relative]
relative_error_lt_conversion [lemma, in Flocq.Prop.Fprop_relative]
relative_error_FLT [lemma, in Flocq.Prop.Fprop_relative]
relative_error_N_round_F2R_emin [lemma, in Flocq.Prop.Fprop_relative]
relative_error_ex [lemma, in Flocq.Prop.Fprop_relative]
relative_error_N_FLX [lemma, in Flocq.Prop.Fprop_relative]
relative_error_N_FLT_round [lemma, in Flocq.Prop.Fprop_relative]
relative_error_F2R_emin_ex [lemma, in Flocq.Prop.Fprop_relative]
relative_error_FLX_ex [lemma, in Flocq.Prop.Fprop_relative]
relative_error_N_FLX_round [lemma, in Flocq.Prop.Fprop_relative]
relative_error_N_FLT_F2R_emin [lemma, in Flocq.Prop.Fprop_relative]
relative_error_F2R_emin [lemma, in Flocq.Prop.Fprop_relative]
relative_error [lemma, in Flocq.Prop.Fprop_relative]
relative_error_FLX_aux [lemma, in Flocq.Prop.Fprop_relative]
relative_error_FLX [lemma, in Flocq.Prop.Fprop_relative]
relative_error_FLT_ex [lemma, in Flocq.Prop.Fprop_relative]
relative_error_FLT_aux [lemma, in Flocq.Prop.Fprop_relative]
relative_error_N_FLT_F2R_emin_ex [lemma, in Flocq.Prop.Fprop_relative]
Req_bool [definition, in Flocq.Core.Fcore_Raux]
Req_bool_spec [lemma, in Flocq.Core.Fcore_Raux]
Req_bool_true [lemma, in Flocq.Core.Fcore_Raux]
Req_bool [section, in Flocq.Core.Fcore_Raux]
Req_bool_prop [inductive, in Flocq.Core.Fcore_Raux]
Req_bool_false [lemma, in Flocq.Core.Fcore_Raux]
Req_bool_false_ [constructor, in Flocq.Core.Fcore_Raux]
Req_bool_true_ [constructor, in Flocq.Core.Fcore_Raux]
Rinv_lt [lemma, in Flocq.Core.Fcore_Raux]
Rinv_le [lemma, in Flocq.Core.Fcore_Raux]
Rle_bool [section, in Flocq.Core.Fcore_Raux]
Rle_0_minus [lemma, in Flocq.Core.Fcore_Raux]
Rle_bool_prop [inductive, in Flocq.Core.Fcore_Raux]
Rle_bool_false_ [constructor, in Flocq.Core.Fcore_Raux]
Rle_bool_true_ [constructor, in Flocq.Core.Fcore_Raux]
Rle_bool_false [lemma, in Flocq.Core.Fcore_Raux]
Rle_bool [definition, in Flocq.Core.Fcore_Raux]
Rle_bool_spec [lemma, in Flocq.Core.Fcore_Raux]
Rle_bool_true [lemma, in Flocq.Core.Fcore_Raux]
Rlt_bool_false [lemma, in Flocq.Core.Fcore_Raux]
Rlt_bool [definition, in Flocq.Core.Fcore_Raux]
Rlt_bool_spec [lemma, in Flocq.Core.Fcore_Raux]
Rlt_bool [section, in Flocq.Core.Fcore_Raux]
Rlt_bool_prop [inductive, in Flocq.Core.Fcore_Raux]
Rlt_bool_false_ [constructor, in Flocq.Core.Fcore_Raux]
Rlt_bool_true_ [constructor, in Flocq.Core.Fcore_Raux]
Rlt_bool_true [lemma, in Flocq.Core.Fcore_Raux]
Rmin_compare [lemma, in Flocq.Core.Fcore_Raux]
Rmissing [section, in Flocq.Core.Fcore_Raux]
Rmult_eq_reg_r [lemma, in Flocq.Core.Fcore_Raux]
Rmult_minus_distr_r [lemma, in Flocq.Core.Fcore_Raux]
Rmult_le_reg_r [lemma, in Flocq.Core.Fcore_Raux]
Rmult_min_distr_r [lemma, in Flocq.Core.Fcore_Raux]
Rmult_lt_reg_r [lemma, in Flocq.Core.Fcore_Raux]
Rmult_min_distr_l [lemma, in Flocq.Core.Fcore_Raux]
RND [section, in Flocq.Core.Fcore_defs]
rndDN [abbreviation, in Flocq.Core.Fcore_generic_fmt]
rndNA [abbreviation, in Flocq.Core.Fcore_generic_fmt]
rndNE [abbreviation, in Flocq.Core.Fcore_rnd_ne]
rndUP [abbreviation, in Flocq.Core.Fcore_generic_fmt]
rndZR [abbreviation, in Flocq.Core.Fcore_generic_fmt]
Rnd_DN_pt_idempotent [lemma, in Flocq.Core.Fcore_rnd]
Rnd_ZR_pt [definition, in Flocq.Core.Fcore_defs]
Rnd_DN_UP_pt_N [lemma, in Flocq.Core.Fcore_rnd]
Rnd_NA_pt_monotone [lemma, in Flocq.Core.Fcore_rnd]
Rnd_NA_unicity [lemma, in Flocq.Core.Fcore_rnd]
Rnd_ZR [definition, in Flocq.Core.Fcore_defs]
Rnd_NA [definition, in Flocq.Core.Fcore_defs]
Rnd_NA_pt [definition, in Flocq.Core.Fcore_defs]
Rnd_DN_pt_monotone [lemma, in Flocq.Core.Fcore_rnd]
Rnd_N_pt_refl [lemma, in Flocq.Core.Fcore_rnd]
Rnd_NG_pt_refl [lemma, in Flocq.Core.Fcore_rnd]
RND_prop [section, in Flocq.Core.Fcore_rnd]
RND_FIX.beta [variable, in Flocq.Core.Fcore_FIX]
RND_FLT.NE_prop [variable, in Flocq.Core.Fcore_FLT]
Rnd_ZR_abs [lemma, in Flocq.Core.Fcore_rnd]
RND_FIX [section, in Flocq.Core.Fcore_FIX]
Rnd_N_pt_0 [lemma, in Flocq.Core.Fcore_rnd]
RND_FLT.emin [variable, in Flocq.Core.Fcore_FLT]
RND_FIX.emin [variable, in Flocq.Core.Fcore_FIX]
RND_FLX.beta [variable, in Flocq.Core.Fcore_FLX]
RND_FTZ.beta [variable, in Flocq.Core.Fcore_FTZ]
Rnd_N_pt_DN_or_UP_eq [lemma, in Flocq.Core.Fcore_rnd]
Rnd_UP_pt_refl [lemma, in Flocq.Core.Fcore_rnd]
RND_FLX [section, in Flocq.Core.Fcore_FLX]
RND_FTZ.FTZ_round [section, in Flocq.Core.Fcore_FTZ]
RND_FTZ [section, in Flocq.Core.Fcore_FTZ]
Rnd_DN_pt_equiv_format [lemma, in Flocq.Core.Fcore_rnd]
Rnd_DN_pt_unicity [lemma, in Flocq.Core.Fcore_rnd]
Rnd_N [definition, in Flocq.Core.Fcore_defs]
RND_FTZ.prec [variable, in Flocq.Core.Fcore_FTZ]
Rnd_UP_pt [definition, in Flocq.Core.Fcore_defs]
Rnd_UP_pt_unicity [lemma, in Flocq.Core.Fcore_rnd]
Rnd_NA_pt_refl [lemma, in Flocq.Core.Fcore_rnd]
Rnd_NG_pt_monotone [lemma, in Flocq.Core.Fcore_rnd]
Rnd_DN_pt [definition, in Flocq.Core.Fcore_defs]
Rnd_NE_pt_round [lemma, in Flocq.Core.Fcore_rnd_ne]
RND_FLX.NE_prop [variable, in Flocq.Core.Fcore_FLX]
Rnd_NG_pt_unicity_prop [definition, in Flocq.Core.Fcore_rnd]
Rnd_NG [definition, in Flocq.Core.Fcore_defs]
Rnd_NA_N_pt [lemma, in Flocq.Core.Fcore_rnd]
Rnd_N_pt_idempotent [lemma, in Flocq.Core.Fcore_rnd]
Rnd_N_pt_neg [lemma, in Flocq.Core.Fcore_rnd]
Rnd_ZR_pt_monotone [lemma, in Flocq.Core.Fcore_rnd]
Rnd_NE_pt [definition, in Flocq.Core.Fcore_rnd_ne]
Rnd_UP [definition, in Flocq.Core.Fcore_defs]
Rnd_NG_pt_unicity [lemma, in Flocq.Core.Fcore_rnd]
Rnd_NG_pt [definition, in Flocq.Core.Fcore_defs]
Rnd_N_pt_DN_or_UP [lemma, in Flocq.Core.Fcore_rnd]
Rnd_NA_pt_unicity [lemma, in Flocq.Core.Fcore_rnd]
Rnd_N_pt_monotone [lemma, in Flocq.Core.Fcore_rnd]
Rnd_N_pt_sym [lemma, in Flocq.Core.Fcore_rnd]
Rnd_DN_pt_refl [lemma, in Flocq.Core.Fcore_rnd]
Rnd_N_pt_unicity [lemma, in Flocq.Core.Fcore_rnd]
Rnd_N_pt [definition, in Flocq.Core.Fcore_defs]
Rnd_N_pt_pos [lemma, in Flocq.Core.Fcore_rnd]
Rnd_NG_unicity [lemma, in Flocq.Core.Fcore_rnd]
Rnd_NG_pt_sym [lemma, in Flocq.Core.Fcore_rnd]
Rnd_UP_pt_idempotent [lemma, in Flocq.Core.Fcore_rnd]
Rnd_DN_UP_sym [lemma, in Flocq.Core.Fcore_rnd]
RND_FLX.prec [variable, in Flocq.Core.Fcore_FLX]
Rnd_NA_NG_pt [lemma, in Flocq.Core.Fcore_rnd]
RND_FTZ.emin [variable, in Flocq.Core.Fcore_FTZ]
RND_FLT.prec [variable, in Flocq.Core.Fcore_FLT]
RND_FTZ.FTZ_round.rnd [variable, in Flocq.Core.Fcore_FTZ]
Rnd_DN [definition, in Flocq.Core.Fcore_defs]
Rnd_NA_pt_unicity_prop [lemma, in Flocq.Core.Fcore_rnd]
Rnd_UP_DN_pt_sym [lemma, in Flocq.Core.Fcore_rnd]
Rnd_DN_unicity [lemma, in Flocq.Core.Fcore_rnd]
Rnd_NE_pt_monotone [lemma, in Flocq.Core.Fcore_rnd_ne]
Rnd_UP_pt_monotone [lemma, in Flocq.Core.Fcore_rnd]
Rnd_DN_pt_N [lemma, in Flocq.Core.Fcore_rnd]
Rnd_N_pt_abs [lemma, in Flocq.Core.Fcore_rnd]
Rnd_DN_UP_pt_split [lemma, in Flocq.Core.Fcore_rnd]
Rnd_NA_pt_idempotent [lemma, in Flocq.Core.Fcore_rnd]
Rnd_UP_pt_N [lemma, in Flocq.Core.Fcore_rnd]
Rnd_NE_pt_total [lemma, in Flocq.Core.Fcore_rnd_ne]
Rnd_UP_unicity [lemma, in Flocq.Core.Fcore_rnd]
RND_FLT.beta [variable, in Flocq.Core.Fcore_FLT]
Rnd_DN_UP_pt_sym [lemma, in Flocq.Core.Fcore_rnd]
RND_FLT [section, in Flocq.Core.Fcore_FLT]
Rnd_UP_pt_equiv_format [lemma, in Flocq.Core.Fcore_rnd]
round [definition, in Flocq.Core.Fcore_generic_fmt]
round_trunc_NA_correct [definition, in Flocq.Calc.Fcalc_round]
round_pred_total [definition, in Flocq.Core.Fcore_defs]
round_UP_pt [lemma, in Flocq.Core.Fcore_generic_fmt]
round_sign_any_correct [lemma, in Flocq.Calc.Fcalc_round]
round_DN_pred [lemma, in Flocq.Core.Fcore_ulp]
round_sign_NA_correct [definition, in Flocq.Calc.Fcalc_round]
round_pred [definition, in Flocq.Core.Fcore_defs]
round_trunc_sign_NA_correct [definition, in Flocq.Calc.Fcalc_round]
round_UP_opp [lemma, in Flocq.Core.Fcore_generic_fmt]
round_trunc_sign_DN_correct [definition, in Flocq.Calc.Fcalc_round]
round_sign_DN_correct [definition, in Flocq.Calc.Fcalc_round]
round_ZR_pt [lemma, in Flocq.Core.Fcore_generic_fmt]
round_DN_succ [lemma, in Flocq.Core.Fcore_ulp]
round_generic [lemma, in Flocq.Core.Fcore_generic_fmt]
round_bounded_small_pos [lemma, in Flocq.Core.Fcore_generic_fmt]
round_UP_pred [lemma, in Flocq.Core.Fcore_ulp]
round_le_generic [lemma, in Flocq.Core.Fcore_generic_fmt]
round_trunc_sign_any_correct [lemma, in Flocq.Calc.Fcalc_round]
round_UP [definition, in Flocq.Calc.Fcalc_round]
round_UP_succ [lemma, in Flocq.Core.Fcore_ulp]
round_N_pt [lemma, in Flocq.Core.Fcore_generic_fmt]
round_sign_UP [definition, in Flocq.Calc.Fcalc_round]
round_DN_pt [lemma, in Flocq.Core.Fcore_generic_fmt]
round_large_pos_ge_pow [lemma, in Flocq.Core.Fcore_generic_fmt]
round_abs_abs [lemma, in Flocq.Core.Fcore_generic_fmt]
round_opp [lemma, in Flocq.Core.Fcore_generic_fmt]
round_N_middle [lemma, in Flocq.Core.Fcore_generic_fmt]
round_NE_pt [lemma, in Flocq.Core.Fcore_rnd_ne]
round_mode [definition, in Flocq.Appli.Fappli_IEEE]
round_ext [lemma, in Flocq.Core.Fcore_generic_fmt]
round_DN_or_UP [lemma, in Flocq.Core.Fcore_generic_fmt]
round_0 [lemma, in Flocq.Core.Fcore_generic_fmt]
round_pred_le_0 [lemma, in Flocq.Core.Fcore_rnd]
round_trunc_sign_NE_correct [definition, in Flocq.Calc.Fcalc_round]
round_pred_monotone [definition, in Flocq.Core.Fcore_defs]
round_pred_lt_0 [lemma, in Flocq.Core.Fcore_rnd]
round_UP_small_pos [lemma, in Flocq.Core.Fcore_generic_fmt]
round_bounded_large_pos [lemma, in Flocq.Core.Fcore_generic_fmt]
round_N_opp [lemma, in Flocq.Core.Fcore_generic_fmt]
round_unicity [lemma, in Flocq.Core.Fcore_rnd]
round_UP_correct [definition, in Flocq.Calc.Fcalc_round]
round_NE_opp [lemma, in Flocq.Core.Fcore_rnd_ne]
round_NA_pt [lemma, in Flocq.Core.Fcore_generic_fmt]
round_NE_pt_pos [lemma, in Flocq.Core.Fcore_rnd_ne]
round_NA_correct [definition, in Flocq.Calc.Fcalc_round]
round_val_of_pred [lemma, in Flocq.Core.Fcore_rnd]
round_FTZ_FLX [lemma, in Flocq.Core.Fcore_FTZ]
round_NE_correct [definition, in Flocq.Calc.Fcalc_round]
round_FLT_FLX [lemma, in Flocq.Core.Fcore_FLT]
round_ZR_correct [definition, in Flocq.Calc.Fcalc_round]
round_trunc_UP_correct [definition, in Flocq.Calc.Fcalc_round]
round_N [definition, in Flocq.Calc.Fcalc_round]
round_sign_ZR_correct [definition, in Flocq.Calc.Fcalc_round]
round_FTZ_small [lemma, in Flocq.Core.Fcore_FTZ]
round_pred_ge_0 [lemma, in Flocq.Core.Fcore_rnd]
round_plus_eq_zero [lemma, in Flocq.Prop.Fprop_plus_error]
round_sign_NE_correct [definition, in Flocq.Calc.Fcalc_round]
round_le_pos [lemma, in Flocq.Core.Fcore_generic_fmt]
round_ZR [definition, in Flocq.Calc.Fcalc_round]
round_trunc_any_correct [lemma, in Flocq.Calc.Fcalc_round]
round_pred_gt_0 [lemma, in Flocq.Core.Fcore_rnd]
round_repr_same_exp [lemma, in Flocq.Prop.Fprop_plus_error]
round_le [lemma, in Flocq.Core.Fcore_generic_fmt]
round_trunc_DN_correct [definition, in Flocq.Calc.Fcalc_round]
round_ge_generic [lemma, in Flocq.Core.Fcore_generic_fmt]
round_trunc_sign_ZR_correct [definition, in Flocq.Calc.Fcalc_round]
round_trunc_NE_correct [definition, in Flocq.Calc.Fcalc_round]
round_fun_of_pred [lemma, in Flocq.Core.Fcore_rnd]
round_DN_small_pos [lemma, in Flocq.Core.Fcore_generic_fmt]
round_sign_DN [definition, in Flocq.Calc.Fcalc_round]
round_DN_correct [definition, in Flocq.Calc.Fcalc_round]
round_any_correct [lemma, in Flocq.Calc.Fcalc_round]
round_plus_eq_zero_aux [lemma, in Flocq.Prop.Fprop_plus_error]
round_trunc_ZR_correct [definition, in Flocq.Calc.Fcalc_round]
round_trunc_sign_UP_correct [definition, in Flocq.Calc.Fcalc_round]
round_sign_UP_correct [definition, in Flocq.Calc.Fcalc_round]
round_DN_opp [lemma, in Flocq.Core.Fcore_generic_fmt]
Rplus_eq_reg_r [lemma, in Flocq.Core.Fcore_Raux]
Rplus_le_reg_r [lemma, in Flocq.Core.Fcore_Raux]


S

Same_sign [section, in Flocq.Core.Fcore_Zaux]
satisfies_any_imp_NA [lemma, in Flocq.Core.Fcore_rnd]
satisfies_any_imp_ZR [lemma, in Flocq.Core.Fcore_rnd]
satisfies_any_eq [lemma, in Flocq.Core.Fcore_rnd]
satisfies_any_imp_DN [lemma, in Flocq.Core.Fcore_rnd]
Satisfies_any [constructor, in Flocq.Core.Fcore_rnd]
satisfies_any_imp_UP [lemma, in Flocq.Core.Fcore_rnd]
satisfies_any_imp_NG [lemma, in Flocq.Core.Fcore_rnd]
satisfies_any [inductive, in Flocq.Core.Fcore_rnd]
scaled_mantissa_mult_bpow [lemma, in Flocq.Core.Fcore_generic_fmt]
scaled_mantissa_abs [lemma, in Flocq.Core.Fcore_generic_fmt]
scaled_mantissa_small [lemma, in Flocq.Core.Fcore_generic_fmt]
scaled_mantissa_DN [lemma, in Flocq.Core.Fcore_generic_fmt]
scaled_mantissa_opp [lemma, in Flocq.Core.Fcore_generic_fmt]
scaled_mantissa_generic [lemma, in Flocq.Core.Fcore_generic_fmt]
scaled_mantissa_0 [lemma, in Flocq.Core.Fcore_generic_fmt]
scaled_mantissa [definition, in Flocq.Core.Fcore_generic_fmt]
shl_align_correct [lemma, in Flocq.Appli.Fappli_IEEE]
shl_align [definition, in Flocq.Appli.Fappli_IEEE]
shl_align_fexp [definition, in Flocq.Appli.Fappli_IEEE]
shl_align_fexp_correct [lemma, in Flocq.Appli.Fappli_IEEE]
shr [definition, in Flocq.Appli.Fappli_IEEE]
shr_s [projection, in Flocq.Appli.Fappli_IEEE]
shr_1 [definition, in Flocq.Appli.Fappli_IEEE]
shr_m_shr_record_of_loc [lemma, in Flocq.Appli.Fappli_IEEE]
shr_m [projection, in Flocq.Appli.Fappli_IEEE]
shr_record [record, in Flocq.Appli.Fappli_IEEE]
shr_truncate [lemma, in Flocq.Appli.Fappli_IEEE]
shr_record_of_loc [definition, in Flocq.Appli.Fappli_IEEE]
shr_r [projection, in Flocq.Appli.Fappli_IEEE]
shr_fexp [definition, in Flocq.Appli.Fappli_IEEE]
sign_FF [definition, in Flocq.Appli.Fappli_IEEE]
snd_shl_align [lemma, in Flocq.Appli.Fappli_IEEE]
split_bits_of_binary_float [definition, in Flocq.Appli.Fappli_IEEE_bits]
split_bits_of_binary_float_correct [lemma, in Flocq.Appli.Fappli_IEEE_bits]
split_join_bits [lemma, in Flocq.Appli.Fappli_IEEE_bits]
split_bits [definition, in Flocq.Appli.Fappli_IEEE_bits]
split_bits_inj [lemma, in Flocq.Appli.Fappli_IEEE_bits]
sqrt_error_FLX_N [lemma, in Flocq.Prop.Fprop_div_sqrt_error]
sqrt_ge_0 [lemma, in Flocq.Core.Fcore_Raux]
sterbenz [lemma, in Flocq.Prop.Fprop_Sterbenz]
sterbenz_aux [lemma, in Flocq.Prop.Fprop_Sterbenz]
subnormal_exponent [lemma, in Flocq.Core.Fcore_generic_fmt]
succ_le_lt [lemma, in Flocq.Core.Fcore_ulp]
succ_le_bpow [lemma, in Flocq.Core.Fcore_ulp]


T

truncate [definition, in Flocq.Calc.Fcalc_round]
truncate_0 [lemma, in Flocq.Calc.Fcalc_round]
truncate_FIX [definition, in Flocq.Calc.Fcalc_round]
truncate_aux_comp [lemma, in Flocq.Calc.Fcalc_round]
truncate_aux [definition, in Flocq.Calc.Fcalc_round]
truncate_correct [lemma, in Flocq.Calc.Fcalc_round]
truncate_correct_partial [lemma, in Flocq.Calc.Fcalc_round]
truncate_correct_format [lemma, in Flocq.Calc.Fcalc_round]
truncate_FIX_correct [lemma, in Flocq.Calc.Fcalc_round]


U

ulp [definition, in Flocq.Core.Fcore_ulp]
ulp_half_error_f [lemma, in Flocq.Core.Fcore_ulp]
ulp_bpow [lemma, in Flocq.Core.Fcore_ulp]
ulp_abs [lemma, in Flocq.Core.Fcore_ulp]
ulp_half_error [lemma, in Flocq.Core.Fcore_ulp]
ulp_DN_UP [lemma, in Flocq.Core.Fcore_ulp]
ulp_error [lemma, in Flocq.Core.Fcore_ulp]
ulp_error_f [lemma, in Flocq.Core.Fcore_ulp]
ulp_le_id [lemma, in Flocq.Core.Fcore_ulp]
ulp_le [lemma, in Flocq.Core.Fcore_ulp]
ulp_le_abs [lemma, in Flocq.Core.Fcore_ulp]
ulp_opp [lemma, in Flocq.Core.Fcore_ulp]
ulp_DN [lemma, in Flocq.Core.Fcore_ulp]


V

valid_exp [projection, in Flocq.Core.Fcore_generic_fmt]
valid_exp [constructor, in Flocq.Core.Fcore_generic_fmt]
valid_rnd_FTZ [instance, in Flocq.Core.Fcore_FTZ]
valid_rnd_UP [instance, in Flocq.Core.Fcore_generic_fmt]
valid_rnd_NA [instance, in Flocq.Core.Fcore_generic_fmt]
valid_rnd_N [instance, in Flocq.Core.Fcore_generic_fmt]
valid_rnd_ZR [instance, in Flocq.Core.Fcore_generic_fmt]
Valid_exp [record, in Flocq.Core.Fcore_generic_fmt]
Valid_exp [inductive, in Flocq.Core.Fcore_generic_fmt]
valid_rnd_round_mode [instance, in Flocq.Appli.Fappli_IEEE]
valid_binary_B2FF [lemma, in Flocq.Appli.Fappli_IEEE]
valid_rnd_DN [instance, in Flocq.Core.Fcore_generic_fmt]
valid_binary [definition, in Flocq.Appli.Fappli_IEEE]
valid_rnd_opp [instance, in Flocq.Core.Fcore_generic_fmt]
Valid_rnd [record, in Flocq.Core.Fcore_generic_fmt]


Z

Zaway [definition, in Flocq.Core.Fcore_Raux]
Zaway_abs [lemma, in Flocq.Core.Fcore_Raux]
Zaway_ceil [lemma, in Flocq.Core.Fcore_Raux]
Zaway_le [lemma, in Flocq.Core.Fcore_Raux]
Zaway_opp [lemma, in Flocq.Core.Fcore_Raux]
Zaway_floor [lemma, in Flocq.Core.Fcore_Raux]
Zaway_Z2R [lemma, in Flocq.Core.Fcore_Raux]
Zceil [definition, in Flocq.Core.Fcore_Raux]
Zceil_Z2R [lemma, in Flocq.Core.Fcore_Raux]
Zceil_le [lemma, in Flocq.Core.Fcore_Raux]
Zceil_imp [lemma, in Flocq.Core.Fcore_Raux]
Zceil_ub [lemma, in Flocq.Core.Fcore_Raux]
Zceil_glb [lemma, in Flocq.Core.Fcore_Raux]
Zceil_floor_neq [lemma, in Flocq.Core.Fcore_Raux]
Zcompare [section, in Flocq.Core.Fcore_Zaux]
Zcompare_prop [inductive, in Flocq.Core.Fcore_Zaux]
Zcompare_Lt_ [constructor, in Flocq.Core.Fcore_Zaux]
Zcompare_spec [lemma, in Flocq.Core.Fcore_Zaux]
Zcompare_Lt [lemma, in Flocq.Core.Fcore_Zaux]
Zcompare_Eq_ [constructor, in Flocq.Core.Fcore_Zaux]
Zcompare_Eq [lemma, in Flocq.Core.Fcore_Zaux]
Zcompare_Gt_ [constructor, in Flocq.Core.Fcore_Zaux]
Zcompare_Gt [lemma, in Flocq.Core.Fcore_Zaux]
Zdigit [definition, in Flocq.Core.Fcore_digits]
Zdigits [definition, in Flocq.Core.Fcore_digits]
Zdigits_mult_strong [lemma, in Flocq.Calc.Fcalc_digits]
Zdigits_aux [definition, in Flocq.Core.Fcore_digits]
Zdigits_ln_beta [lemma, in Flocq.Calc.Fcalc_digits]
Zdigits_Zpower [lemma, in Flocq.Calc.Fcalc_digits]
Zdigits_slice [lemma, in Flocq.Core.Fcore_digits]
Zdigits_correct [lemma, in Flocq.Core.Fcore_digits]
Zdigits_mult_Zpower [lemma, in Flocq.Calc.Fcalc_digits]
Zdigits_abs [lemma, in Flocq.Core.Fcore_digits]
Zdigits_ge_0 [lemma, in Flocq.Core.Fcore_digits]
Zdigits_gt_0 [lemma, in Flocq.Core.Fcore_digits]
Zdigits_gt_Zpower [lemma, in Flocq.Calc.Fcalc_digits]
Zdigits_mult [lemma, in Flocq.Calc.Fcalc_digits]
Zdigits_le_Zpower [lemma, in Flocq.Calc.Fcalc_digits]
Zdigits_le [lemma, in Flocq.Calc.Fcalc_digits]
Zdigits_div_Zpower [lemma, in Flocq.Calc.Fcalc_digits]
Zdigits_mult_ge [lemma, in Flocq.Calc.Fcalc_digits]
Zdigits2 [definition, in Flocq.Appli.Fappli_IEEE]
Zdigits2_Zdigits [lemma, in Flocq.Appli.Fappli_IEEE]
Zdigit_scale [lemma, in Flocq.Core.Fcore_digits]
Zdigit_mod_pow_out [lemma, in Flocq.Core.Fcore_digits]
Zdigit_mul_pow [lemma, in Flocq.Core.Fcore_digits]
Zdigit_not_0 [lemma, in Flocq.Core.Fcore_digits]
Zdigit_out [lemma, in Flocq.Core.Fcore_digits]
Zdigit_div_pow [lemma, in Flocq.Core.Fcore_digits]
Zdigit_slice_out [lemma, in Flocq.Core.Fcore_digits]
Zdigit_lt [lemma, in Flocq.Core.Fcore_digits]
Zdigit_mod_pow [lemma, in Flocq.Core.Fcore_digits]
Zdigit_0 [lemma, in Flocq.Core.Fcore_digits]
Zdigit_ge_Zpower_pos [lemma, in Flocq.Core.Fcore_digits]
Zdigit_slice [lemma, in Flocq.Core.Fcore_digits]
Zdigit_digits [lemma, in Flocq.Core.Fcore_digits]
Zdigit_ext [lemma, in Flocq.Core.Fcore_digits]
Zdigit_not_0_pos [lemma, in Flocq.Core.Fcore_digits]
Zdigit_opp [lemma, in Flocq.Core.Fcore_digits]
Zdigit_ge_Zpower [lemma, in Flocq.Core.Fcore_digits]
Zdigit_plus [lemma, in Flocq.Core.Fcore_digits]
Zdiv_Rdiv [section, in Flocq.Core.Fcore_Raux]
Zdiv_mod_mult [lemma, in Flocq.Core.Fcore_Zaux]
Zeq_bool_true_ [constructor, in Flocq.Core.Fcore_Zaux]
Zeq_bool_false [lemma, in Flocq.Core.Fcore_Zaux]
Zeq_bool_false_ [constructor, in Flocq.Core.Fcore_Zaux]
Zeq_bool_prop [inductive, in Flocq.Core.Fcore_Zaux]
Zeq_bool_true [lemma, in Flocq.Core.Fcore_Zaux]
Zeq_bool [section, in Flocq.Core.Fcore_Zaux]
Zeq_bool_spec [lemma, in Flocq.Core.Fcore_Zaux]
Zeven [definition, in Flocq.Core.Fcore_Zaux]
Zeven_Zpower_odd [lemma, in Flocq.Core.Fcore_Zaux]
Zeven_ex [lemma, in Flocq.Core.Fcore_Zaux]
Zeven_2xp1 [lemma, in Flocq.Core.Fcore_Zaux]
Zeven_mult [lemma, in Flocq.Core.Fcore_Zaux]
Zeven_opp [lemma, in Flocq.Core.Fcore_Zaux]
Zeven_Zpower [lemma, in Flocq.Core.Fcore_Zaux]
Zeven_plus [lemma, in Flocq.Core.Fcore_Zaux]
Zfloor [definition, in Flocq.Core.Fcore_Raux]
Zfloor_ub [lemma, in Flocq.Core.Fcore_Raux]
Zfloor_imp [lemma, in Flocq.Core.Fcore_Raux]
Zfloor_div [lemma, in Flocq.Core.Fcore_Raux]
Zfloor_lb [lemma, in Flocq.Core.Fcore_Raux]
Zfloor_lub [lemma, in Flocq.Core.Fcore_Raux]
Zfloor_le [lemma, in Flocq.Core.Fcore_Raux]
Zfloor_Z2R [lemma, in Flocq.Core.Fcore_Raux]
Zgt_not_eq [lemma, in Flocq.Core.Fcore_Zaux]
Zle_bool_false [lemma, in Flocq.Core.Fcore_Zaux]
Zle_bool_prop [inductive, in Flocq.Core.Fcore_Zaux]
Zle_bool [section, in Flocq.Core.Fcore_Zaux]
Zle_bool_false_ [constructor, in Flocq.Core.Fcore_Zaux]
Zle_bool_true_ [constructor, in Flocq.Core.Fcore_Zaux]
Zle_bool_spec [lemma, in Flocq.Core.Fcore_Zaux]
Zle_bool_true [lemma, in Flocq.Core.Fcore_Zaux]
Zlt_bool_true [lemma, in Flocq.Core.Fcore_Zaux]
Zlt_bool_true_ [constructor, in Flocq.Core.Fcore_Zaux]
Zlt_bool_spec [lemma, in Flocq.Core.Fcore_Zaux]
Zlt_bool_false [lemma, in Flocq.Core.Fcore_Zaux]
Zlt_bool_prop [inductive, in Flocq.Core.Fcore_Zaux]
Zlt_bool [section, in Flocq.Core.Fcore_Zaux]
Zlt_bool_false_ [constructor, in Flocq.Core.Fcore_Zaux]
Zmissing [section, in Flocq.Core.Fcore_Zaux]
Zmod_mod_mult [lemma, in Flocq.Core.Fcore_Zaux]
Znearest [definition, in Flocq.Core.Fcore_generic_fmt]
ZnearestA [abbreviation, in Flocq.Core.Fcore_generic_fmt]
ZnearestE [abbreviation, in Flocq.Core.Fcore_rnd_ne]
Znearest_ge_floor [lemma, in Flocq.Core.Fcore_generic_fmt]
Znearest_N [lemma, in Flocq.Core.Fcore_generic_fmt]
Znearest_opp [lemma, in Flocq.Core.Fcore_generic_fmt]
Znearest_le_ceil [lemma, in Flocq.Core.Fcore_generic_fmt]
Znearest_N_strict [lemma, in Flocq.Core.Fcore_generic_fmt]
Znearest_DN_or_UP [lemma, in Flocq.Core.Fcore_generic_fmt]
ZOdiv_small_abs [lemma, in Flocq.Core.Fcore_Zaux]
ZOdiv_plus [lemma, in Flocq.Core.Fcore_Zaux]
ZOdiv_plus_pow_digit [lemma, in Flocq.Core.Fcore_digits]
ZOdiv_mod_mult [lemma, in Flocq.Core.Fcore_Zaux]
ZOmod_eq [lemma, in Flocq.Core.Fcore_Zaux]
ZOmod_small_abs [lemma, in Flocq.Core.Fcore_Zaux]
ZOmod_plus_pow_digit [lemma, in Flocq.Core.Fcore_digits]
ZOmod_mod_mult [lemma, in Flocq.Core.Fcore_Zaux]
Zopp_le_cancel [lemma, in Flocq.Core.Fcore_Zaux]
Zplus_slice [lemma, in Flocq.Core.Fcore_digits]
Zpower [section, in Flocq.Core.Fcore_Zaux]
Zpower_nat_S [lemma, in Flocq.Core.Fcore_Zaux]
Zpower_ge_0 [lemma, in Flocq.Core.Fcore_Zaux]
Zpower_lt_Zpower [lemma, in Flocq.Core.Fcore_Zaux]
Zpower_le_Zdigits [lemma, in Flocq.Calc.Fcalc_digits]
Zpower_pos_gt_0 [lemma, in Flocq.Core.Fcore_Zaux]
Zpower_gt_1 [lemma, in Flocq.Core.Fcore_Zaux]
Zpower_plus [lemma, in Flocq.Core.Fcore_Zaux]
Zpower_le [lemma, in Flocq.Core.Fcore_Zaux]
Zpower_lt [lemma, in Flocq.Core.Fcore_Zaux]
Zpower_Zpower_nat [lemma, in Flocq.Core.Fcore_Zaux]
Zpower_gt_id [lemma, in Flocq.Core.Fcore_digits]
Zpower_gt_0 [lemma, in Flocq.Core.Fcore_Zaux]
Zpower_gt_Zdigits [lemma, in Flocq.Calc.Fcalc_digits]
Zpower.r [variable, in Flocq.Core.Fcore_Zaux]
Zrnd_FTZ [definition, in Flocq.Core.Fcore_FTZ]
Zrnd_le [projection, in Flocq.Core.Fcore_generic_fmt]
Zrnd_DN_or_UP [lemma, in Flocq.Core.Fcore_generic_fmt]
Zrnd_opp [definition, in Flocq.Core.Fcore_generic_fmt]
Zrnd_Z2R [projection, in Flocq.Core.Fcore_generic_fmt]
Zsame_sign_imp [lemma, in Flocq.Core.Fcore_Zaux]
Zsame_sign_scale [lemma, in Flocq.Core.Fcore_digits]
Zsame_sign_odiv [lemma, in Flocq.Core.Fcore_Zaux]
Zsame_sign_trans_weak [lemma, in Flocq.Core.Fcore_Zaux]
Zsame_sign_slice [lemma, in Flocq.Core.Fcore_digits]
Zsame_sign_trans [lemma, in Flocq.Core.Fcore_Zaux]
Zscale [definition, in Flocq.Core.Fcore_digits]
Zscale_0 [lemma, in Flocq.Core.Fcore_digits]
Zscale_scale [lemma, in Flocq.Core.Fcore_digits]
Zscale_mul_pow [lemma, in Flocq.Core.Fcore_digits]
Zslice [definition, in Flocq.Core.Fcore_digits]
Zslice_mul_pow [lemma, in Flocq.Core.Fcore_digits]
Zslice_slice [lemma, in Flocq.Core.Fcore_digits]
Zslice_div_pow_scale [lemma, in Flocq.Core.Fcore_digits]
Zslice_div_pow [lemma, in Flocq.Core.Fcore_digits]
Zslice_0 [lemma, in Flocq.Core.Fcore_digits]
Zslice_scale [lemma, in Flocq.Core.Fcore_digits]
Zsqrt [definition, in Flocq.Calc.Fcalc_sqrt]
Zsqrt_aux_correct [lemma, in Flocq.Calc.Fcalc_sqrt]
Zsqrt_aux [definition, in Flocq.Calc.Fcalc_sqrt]
Zsqrt_ind [lemma, in Flocq.Calc.Fcalc_sqrt]
Zsqrt_correct [lemma, in Flocq.Calc.Fcalc_sqrt]
Zsum_digit_digit [lemma, in Flocq.Core.Fcore_digits]
Zsum_digit [definition, in Flocq.Core.Fcore_digits]
Ztrunc [definition, in Flocq.Core.Fcore_Raux]
Ztrunc_le [lemma, in Flocq.Core.Fcore_Raux]
Ztrunc_floor [lemma, in Flocq.Core.Fcore_Raux]
Ztrunc_ceil [lemma, in Flocq.Core.Fcore_Raux]
Ztrunc_opp [lemma, in Flocq.Core.Fcore_Raux]
Ztrunc_lub [lemma, in Flocq.Core.Fcore_Raux]
Ztrunc_Z2R [lemma, in Flocq.Core.Fcore_Raux]
Ztrunc_abs [lemma, in Flocq.Core.Fcore_Raux]
Z_of_nat_S_digits2_Pnat [lemma, in Flocq.Calc.Fcalc_digits]
Z2R [definition, in Flocq.Core.Fcore_Raux]
Z2R [section, in Flocq.Core.Fcore_Raux]
Z2R_cond_Zopp [lemma, in Flocq.Core.Fcore_Raux]
Z2R_opp [lemma, in Flocq.Core.Fcore_Raux]
Z2R_Zpower [lemma, in Flocq.Core.Fcore_Raux]
Z2R_Zpower_nat [lemma, in Flocq.Core.Fcore_Raux]
Z2R_abs [lemma, in Flocq.Core.Fcore_Raux]
Z2R_neq [lemma, in Flocq.Core.Fcore_Raux]
Z2R_Zpower_pos [lemma, in Flocq.Core.Fcore_Raux]
Z2R_minus [lemma, in Flocq.Core.Fcore_Raux]
Z2R_mult [lemma, in Flocq.Core.Fcore_Raux]
Z2R_plus [lemma, in Flocq.Core.Fcore_Raux]
Z2R_le [lemma, in Flocq.Core.Fcore_Raux]
Z2R_lt [lemma, in Flocq.Core.Fcore_Raux]
Z2R_IZR [lemma, in Flocq.Core.Fcore_Raux]
Z2R_le_lt [lemma, in Flocq.Core.Fcore_Raux]



Instance Index

E

exists_NE_FLX [in Flocq.Core.Fcore_FLX]
exists_NE_FLT [in Flocq.Core.Fcore_FLT]


F

fexp_monotone [in Flocq.Appli.Fappli_IEEE]
fexp_correct [in Flocq.Appli.Fappli_IEEE]
FIX_exp_monotone [in Flocq.Core.Fcore_FIX]
FIX_exp_valid [in Flocq.Core.Fcore_FIX]
FLT_exp_valid [in Flocq.Core.Fcore_FLT]
FLT_exp_monotone [in Flocq.Core.Fcore_FLT]
FLX_exp_monotone [in Flocq.Core.Fcore_FLX]
FLX_exp_valid [in Flocq.Core.Fcore_FLX]
FTZ_exp_valid [in Flocq.Core.Fcore_FTZ]


M

monotone_exp_not_FTZ [in Flocq.Core.Fcore_generic_fmt]


V

valid_rnd_FTZ [in Flocq.Core.Fcore_FTZ]
valid_rnd_UP [in Flocq.Core.Fcore_generic_fmt]
valid_rnd_NA [in Flocq.Core.Fcore_generic_fmt]
valid_rnd_N [in Flocq.Core.Fcore_generic_fmt]
valid_rnd_ZR [in Flocq.Core.Fcore_generic_fmt]
valid_rnd_round_mode [in Flocq.Appli.Fappli_IEEE]
valid_rnd_DN [in Flocq.Core.Fcore_generic_fmt]
valid_rnd_opp [in Flocq.Core.Fcore_generic_fmt]



Projection Index

E

exists_NE [in Flocq.Core.Fcore_rnd_ne]
exp_not_FTZ [in Flocq.Core.Fcore_generic_fmt]


F

Fexp [in Flocq.Core.Fcore_defs]
Fnum [in Flocq.Core.Fcore_defs]


L

ln_beta_val [in Flocq.Core.Fcore_Raux]


M

monotone_exp [in Flocq.Core.Fcore_generic_fmt]


P

prec_gt_0 [in Flocq.Core.Fcore_FLX]


R

radix_val [in Flocq.Core.Fcore_Zaux]
radix_prop [in Flocq.Core.Fcore_Zaux]


S

shr_s [in Flocq.Appli.Fappli_IEEE]
shr_m [in Flocq.Appli.Fappli_IEEE]
shr_r [in Flocq.Appli.Fappli_IEEE]


V

valid_exp [in Flocq.Core.Fcore_generic_fmt]


Z

Zrnd_le [in Flocq.Core.Fcore_generic_fmt]
Zrnd_Z2R [in Flocq.Core.Fcore_generic_fmt]



Record Index

E

Exists_NE [in Flocq.Core.Fcore_rnd_ne]
Exp_not_FTZ [in Flocq.Core.Fcore_generic_fmt]


F

float [in Flocq.Core.Fcore_defs]


L

ln_beta_prop [in Flocq.Core.Fcore_Raux]


M

Monotone_exp [in Flocq.Core.Fcore_generic_fmt]


P

Prec_gt_0 [in Flocq.Core.Fcore_FLX]


R

radix [in Flocq.Core.Fcore_Zaux]


S

shr_record [in Flocq.Appli.Fappli_IEEE]


V

Valid_exp [in Flocq.Core.Fcore_generic_fmt]
Valid_rnd [in Flocq.Core.Fcore_generic_fmt]



Lemma Index

A

abs_round_ge_generic [in Flocq.Core.Fcore_generic_fmt]
abs_cond_Zopp [in Flocq.Core.Fcore_Raux]
abs_B2R_lt_emax [in Flocq.Appli.Fappli_IEEE]
abs_round_le_generic [in Flocq.Core.Fcore_generic_fmt]
abs_lt_bpow_prec [in Flocq.Core.Fcore_generic_fmt]
abs_cond_Ropp [in Flocq.Core.Fcore_Raux]


B

Bdiv_correct [in Flocq.Appli.Fappli_IEEE]
Bdiv_correct_aux [in Flocq.Appli.Fappli_IEEE]
binary_float_of_bits_of_binary_float [in Flocq.Appli.Fappli_IEEE_bits]
binary_round_aux_correct [in Flocq.Appli.Fappli_IEEE]
binary_round_correct [in Flocq.Appli.Fappli_IEEE]
binary_normalize_correct [in Flocq.Appli.Fappli_IEEE]
binary_float_of_bits_aux_correct [in Flocq.Appli.Fappli_IEEE_bits]
bits_of_binary_float_of_bits [in Flocq.Appli.Fappli_IEEE_bits]
Bminus_correct [in Flocq.Appli.Fappli_IEEE]
Bmult_correct [in Flocq.Appli.Fappli_IEEE]
Bmult_correct_aux [in Flocq.Appli.Fappli_IEEE]
Bopp_involutive [in Flocq.Appli.Fappli_IEEE]
bounded_canonic_lt_emax [in Flocq.Appli.Fappli_IEEE]
bounded_lt_emax [in Flocq.Appli.Fappli_IEEE]
Bplus_correct [in Flocq.Appli.Fappli_IEEE]
bpow_lt_bpow [in Flocq.Core.Fcore_Raux]
bpow_1 [in Flocq.Core.Fcore_Raux]
bpow_unique [in Flocq.Core.Fcore_Raux]
bpow_plus [in Flocq.Core.Fcore_Raux]
bpow_gt_0 [in Flocq.Core.Fcore_Raux]
bpow_plus1 [in Flocq.Core.Fcore_Raux]
bpow_ge_0 [in Flocq.Core.Fcore_Raux]
bpow_le_F2R_m1 [in Flocq.Core.Fcore_float_prop]
bpow_lt [in Flocq.Core.Fcore_Raux]
bpow_inj [in Flocq.Core.Fcore_Raux]
bpow_opp [in Flocq.Core.Fcore_Raux]
bpow_le [in Flocq.Core.Fcore_Raux]
bpow_le_F2R [in Flocq.Core.Fcore_float_prop]
bpow_exp [in Flocq.Core.Fcore_Raux]
bpow_powerRZ [in Flocq.Core.Fcore_Raux]
Bsign_FF2B [in Flocq.Appli.Fappli_IEEE]
Bsqrt_correct_aux [in Flocq.Appli.Fappli_IEEE]
Bsqrt_correct [in Flocq.Appli.Fappli_IEEE]
B2FF_Bmult [in Flocq.Appli.Fappli_IEEE]
B2FF_FF2B [in Flocq.Appli.Fappli_IEEE]
B2FF_inj [in Flocq.Appli.Fappli_IEEE]
B2R_inj [in Flocq.Appli.Fappli_IEEE]
B2R_Bopp [in Flocq.Appli.Fappli_IEEE]
B2R_FF2B [in Flocq.Appli.Fappli_IEEE]


C

canonic_unicity [in Flocq.Core.Fcore_generic_fmt]
canonic_exp_round_ge [in Flocq.Core.Fcore_generic_fmt]
canonic_exp_fexp_pos [in Flocq.Core.Fcore_generic_fmt]
canonic_exp_FLT_FIX [in Flocq.Core.Fcore_FLT]
canonic_canonic_mantissa [in Flocq.Appli.Fappli_IEEE]
canonic_exp_FLT_FLX [in Flocq.Core.Fcore_FLT]
canonic_exp_DN [in Flocq.Core.Fcore_generic_fmt]
canonic_exp_fexp [in Flocq.Core.Fcore_generic_fmt]
canonic_opp [in Flocq.Core.Fcore_generic_fmt]
canonic_exp_opp [in Flocq.Core.Fcore_generic_fmt]
canonic_exp_abs [in Flocq.Core.Fcore_generic_fmt]
cond_Ropp_Rlt_bool [in Flocq.Core.Fcore_Raux]
cond_Zopp_Zlt_bool [in Flocq.Core.Fcore_Raux]


D

digits2_Pnat_correct [in Flocq.Core.Fcore_digits]
div_error_FLX [in Flocq.Prop.Fprop_div_sqrt_error]
DN_UP_parity_aux [in Flocq.Core.Fcore_rnd_ne]
DN_UP_parity_generic [in Flocq.Core.Fcore_rnd_ne]
DN_UP_parity_generic_pos [in Flocq.Core.Fcore_rnd_ne]


E

eqbool_irrelevance [in Flocq.Core.Fcore_Zaux]
eqb_false [in Flocq.Core.Fcore_Raux]
eqb_sym [in Flocq.Core.Fcore_Raux]
eqb_true [in Flocq.Core.Fcore_Raux]
eq_Z2R [in Flocq.Core.Fcore_Raux]
error_N_FLT_aux [in Flocq.Prop.Fprop_relative]
exp_le [in Flocq.Core.Fcore_Raux]
ex_Fexp_canonic [in Flocq.Prop.Fprop_div_sqrt_error]


F

Falign_spec [in Flocq.Calc.Fcalc_ops]
Falign_spec_exp [in Flocq.Calc.Fcalc_ops]
Fdiv_core_correct [in Flocq.Calc.Fcalc_div]
Fexp_Fplus [in Flocq.Calc.Fcalc_ops]
FF2B_B2FF_valid [in Flocq.Appli.Fappli_IEEE]
FF2B_B2FF [in Flocq.Appli.Fappli_IEEE]
FF2R_B2FF [in Flocq.Appli.Fappli_IEEE]
FIX_format_generic [in Flocq.Core.Fcore_FIX]
FIX_format_satisfies_any [in Flocq.Core.Fcore_FIX]
FIX_format_FLX [in Flocq.Core.Fcore_FLX]
float_distribution_pos [in Flocq.Core.Fcore_float_prop]
FLT_format_generic [in Flocq.Core.Fcore_FLT]
FLT_format_satisfies_any [in Flocq.Core.Fcore_FLT]
FLXN_format_generic [in Flocq.Core.Fcore_FLX]
FLXN_format_satisfies_any [in Flocq.Core.Fcore_FLX]
FLXN_format_FTZ [in Flocq.Core.Fcore_FTZ]
FLX_format_FIX [in Flocq.Core.Fcore_FLX]
FLX_format_satisfies_any [in Flocq.Core.Fcore_FLX]
FLX_format_generic [in Flocq.Core.Fcore_FLX]
Fminus_same_exp [in Flocq.Calc.Fcalc_ops]
Fplus_same_exp [in Flocq.Calc.Fcalc_ops]
Fsqrt_core_correct [in Flocq.Calc.Fcalc_sqrt]
FTZ_format_FLXN [in Flocq.Core.Fcore_FTZ]
FTZ_format_generic [in Flocq.Core.Fcore_FTZ]
FTZ_format_satisfies_any [in Flocq.Core.Fcore_FTZ]
F2R_plus [in Flocq.Calc.Fcalc_ops]
F2R_gt_0_compat [in Flocq.Core.Fcore_float_prop]
F2R_lt_0_reg [in Flocq.Core.Fcore_float_prop]
F2R_prec_normalize [in Flocq.Core.Fcore_float_prop]
F2R_mult [in Flocq.Calc.Fcalc_ops]
F2R_0 [in Flocq.Core.Fcore_float_prop]
F2R_cond_Zopp [in Flocq.Core.Fcore_float_prop]
F2R_change_exp [in Flocq.Core.Fcore_float_prop]
F2R_lt_bpow [in Flocq.Core.Fcore_float_prop]
F2R_gt_0_reg [in Flocq.Core.Fcore_float_prop]
F2R_bpow [in Flocq.Core.Fcore_float_prop]
F2R_lt_0_compat [in Flocq.Core.Fcore_float_prop]
F2R_abs [in Flocq.Calc.Fcalc_ops]
F2R_eq_0_reg [in Flocq.Core.Fcore_float_prop]
F2R_le_0_compat [in Flocq.Core.Fcore_float_prop]
F2R_le_compat [in Flocq.Core.Fcore_float_prop]
F2R_Zabs [in Flocq.Core.Fcore_float_prop]
F2R_lt_reg [in Flocq.Core.Fcore_float_prop]
F2R_Zopp [in Flocq.Core.Fcore_float_prop]
F2R_eq_reg [in Flocq.Core.Fcore_float_prop]
F2R_minus [in Flocq.Calc.Fcalc_ops]
F2R_p1_le_bpow [in Flocq.Core.Fcore_float_prop]
F2R_ge_0_reg [in Flocq.Core.Fcore_float_prop]
F2R_le_0_reg [in Flocq.Core.Fcore_float_prop]
F2R_le_reg [in Flocq.Core.Fcore_float_prop]
F2R_ge_0_compat [in Flocq.Core.Fcore_float_prop]
F2R_lt_compat [in Flocq.Core.Fcore_float_prop]
F2R_eq_compat [in Flocq.Core.Fcore_float_prop]
F2R_opp [in Flocq.Calc.Fcalc_ops]


G

generic_format_FLT_FIX [in Flocq.Core.Fcore_FLT]
generic_format_plus_weak [in Flocq.Prop.Fprop_Sterbenz]
generic_format_truncate [in Flocq.Calc.Fcalc_round]
generic_format_plus_prec [in Flocq.Prop.Fprop_div_sqrt_error]
generic_format_F2R [in Flocq.Core.Fcore_generic_fmt]
generic_format_B2R [in Flocq.Appli.Fappli_IEEE]
generic_format_EM [in Flocq.Core.Fcore_generic_fmt]
generic_format_abs_inv [in Flocq.Core.Fcore_generic_fmt]
generic_format_pred [in Flocq.Core.Fcore_ulp]
generic_format_succ [in Flocq.Core.Fcore_ulp]
generic_format_pred_1 [in Flocq.Core.Fcore_ulp]
generic_inclusion_ge [in Flocq.Core.Fcore_generic_fmt]
generic_inclusion_ln_beta [in Flocq.Core.Fcore_generic_fmt]
generic_format_0 [in Flocq.Core.Fcore_generic_fmt]
generic_format_FIX_FLT [in Flocq.Core.Fcore_FLT]
generic_format_opp [in Flocq.Core.Fcore_generic_fmt]
generic_inclusion_le_ge [in Flocq.Core.Fcore_generic_fmt]
generic_format_FLT [in Flocq.Core.Fcore_FLT]
generic_format_ge_bpow [in Flocq.Core.Fcore_generic_fmt]
generic_format_satisfies_any [in Flocq.Core.Fcore_generic_fmt]
generic_format_FIX [in Flocq.Core.Fcore_FIX]
generic_format_FLX [in Flocq.Core.Fcore_FLX]
generic_format_discrete [in Flocq.Core.Fcore_generic_fmt]
generic_format_FLXN [in Flocq.Core.Fcore_FLX]
generic_inclusion_lt_ge [in Flocq.Core.Fcore_generic_fmt]
generic_format_FLX_FLT [in Flocq.Core.Fcore_FLT]
generic_inclusion [in Flocq.Core.Fcore_generic_fmt]
generic_inclusion_le [in Flocq.Core.Fcore_generic_fmt]
generic_format_abs [in Flocq.Core.Fcore_generic_fmt]
generic_N_pt_DN_or_UP [in Flocq.Core.Fcore_generic_fmt]
generic_format_plus [in Flocq.Prop.Fprop_Sterbenz]
generic_format_FTZ [in Flocq.Core.Fcore_FTZ]
generic_format_bpow_inv [in Flocq.Core.Fcore_generic_fmt]
generic_format_bpow' [in Flocq.Core.Fcore_generic_fmt]
generic_format_FLT_FLX [in Flocq.Core.Fcore_FLT]
generic_format_pred_2 [in Flocq.Core.Fcore_ulp]
generic_format_round_pos [in Flocq.Core.Fcore_generic_fmt]
generic_format_bpow [in Flocq.Core.Fcore_generic_fmt]
generic_format_canonic [in Flocq.Core.Fcore_generic_fmt]
generic_format_round [in Flocq.Core.Fcore_generic_fmt]


I

inbetween_float_round [in Flocq.Calc.Fcalc_round]
inbetween_spec [in Flocq.Calc.Fcalc_bracket]
inbetween_step_Lo_Mi_Eq_odd [in Flocq.Calc.Fcalc_bracket]
inbetween_distance_inexact_abs [in Flocq.Calc.Fcalc_bracket]
inbetween_step_any_Mi_odd [in Flocq.Calc.Fcalc_bracket]
inbetween_float_unique [in Flocq.Calc.Fcalc_bracket]
inbetween_int_UP [in Flocq.Calc.Fcalc_round]
inbetween_float_new_location [in Flocq.Calc.Fcalc_bracket]
inbetween_step_Hi_Mi_even [in Flocq.Calc.Fcalc_bracket]
inbetween_mult_compat [in Flocq.Calc.Fcalc_bracket]
inbetween_float_UP [in Flocq.Calc.Fcalc_round]
inbetween_float_UP_sign [in Flocq.Calc.Fcalc_round]
inbetween_distance_inexact [in Flocq.Calc.Fcalc_bracket]
inbetween_step_Hi [in Flocq.Calc.Fcalc_bracket]
inbetween_float_ZR [in Flocq.Calc.Fcalc_round]
inbetween_int_NE [in Flocq.Calc.Fcalc_round]
inbetween_mult_aux [in Flocq.Calc.Fcalc_bracket]
inbetween_float_round_sign [in Flocq.Calc.Fcalc_round]
inbetween_float_ex [in Flocq.Calc.Fcalc_bracket]
inbetween_bounds [in Flocq.Calc.Fcalc_bracket]
inbetween_int_ZR [in Flocq.Calc.Fcalc_round]
inbetween_float_DN_sign [in Flocq.Calc.Fcalc_round]
inbetween_shr_1 [in Flocq.Appli.Fappli_IEEE]
inbetween_int_ZR_sign [in Flocq.Calc.Fcalc_round]
inbetween_float_ZR_sign [in Flocq.Calc.Fcalc_round]
inbetween_int_N_sign [in Flocq.Calc.Fcalc_round]
inbetween_step_Mi_Mi_even [in Flocq.Calc.Fcalc_bracket]
inbetween_bounds_not_Eq [in Flocq.Calc.Fcalc_bracket]
inbetween_unique [in Flocq.Calc.Fcalc_bracket]
inbetween_float_NA [in Flocq.Calc.Fcalc_round]
inbetween_float_NE_sign [in Flocq.Calc.Fcalc_round]
inbetween_mult_reg [in Flocq.Calc.Fcalc_bracket]
inbetween_int_N [in Flocq.Calc.Fcalc_round]
inbetween_int_NA_sign [in Flocq.Calc.Fcalc_round]
inbetween_step_not_Eq [in Flocq.Calc.Fcalc_bracket]
inbetween_shr [in Flocq.Appli.Fappli_IEEE]
inbetween_int_DN [in Flocq.Calc.Fcalc_round]
inbetween_float_bounds [in Flocq.Calc.Fcalc_bracket]
inbetween_float_new_location_single [in Flocq.Calc.Fcalc_bracket]
inbetween_float_NE [in Flocq.Calc.Fcalc_round]
inbetween_float_DN [in Flocq.Calc.Fcalc_round]
inbetween_int_UP_sign [in Flocq.Calc.Fcalc_round]
inbetween_step_Lo [in Flocq.Calc.Fcalc_bracket]
inbetween_int_NA [in Flocq.Calc.Fcalc_round]
inbetween_ex [in Flocq.Calc.Fcalc_bracket]
inbetween_int_NE_sign [in Flocq.Calc.Fcalc_round]
inbetween_int_DN_sign [in Flocq.Calc.Fcalc_round]
inbetween_step_Lo_not_Eq [in Flocq.Calc.Fcalc_bracket]
is_finite_FF_B2FF [in Flocq.Appli.Fappli_IEEE]
is_finite_FF2B [in Flocq.Appli.Fappli_IEEE]
is_finite_Bopp [in Flocq.Appli.Fappli_IEEE]


J

join_split_bits [in Flocq.Appli.Fappli_IEEE_bits]


L

le_pred_lt_aux [in Flocq.Core.Fcore_ulp]
le_pred_lt [in Flocq.Core.Fcore_ulp]
le_Z2R [in Flocq.Core.Fcore_Raux]
le_bpow [in Flocq.Core.Fcore_Raux]
le_lt_Z2R [in Flocq.Core.Fcore_Raux]
ln_beta_gt_bpow [in Flocq.Core.Fcore_Raux]
ln_beta_opp [in Flocq.Core.Fcore_Raux]
ln_beta_abs [in Flocq.Core.Fcore_Raux]
ln_beta_F2R [in Flocq.Core.Fcore_float_prop]
ln_beta_gt_Zpower [in Flocq.Core.Fcore_Raux]
ln_beta_F2R_Zdigits [in Flocq.Calc.Fcalc_digits]
ln_beta_le_abs [in Flocq.Core.Fcore_Raux]
ln_beta_le [in Flocq.Core.Fcore_Raux]
ln_beta_F2R_bounds [in Flocq.Core.Fcore_float_prop]
ln_beta_bpow [in Flocq.Core.Fcore_Raux]
ln_beta_unique [in Flocq.Core.Fcore_Raux]
ln_beta_le_Zpower [in Flocq.Core.Fcore_Raux]
ln_beta_le_bpow [in Flocq.Core.Fcore_Raux]
ln_beta_succ [in Flocq.Core.Fcore_ulp]
loc_of_shr_record_of_loc [in Flocq.Appli.Fappli_IEEE]
lt_Z2R [in Flocq.Core.Fcore_Raux]
lt_bpow [in Flocq.Core.Fcore_Raux]
lt_Zdigits [in Flocq.Calc.Fcalc_digits]


M

mantissa_UP_small_pos [in Flocq.Core.Fcore_generic_fmt]
mantissa_small_pos [in Flocq.Core.Fcore_generic_fmt]
mantissa_DN_small_pos [in Flocq.Core.Fcore_generic_fmt]
match_FF2B [in Flocq.Appli.Fappli_IEEE]
middle_range [in Flocq.Calc.Fcalc_bracket]
middle_odd [in Flocq.Calc.Fcalc_bracket]
minus_IZR [in Flocq.Core.Fcore_Raux]
mult_error_FLX [in Flocq.Prop.Fprop_mult_error]
mult_error_FLT [in Flocq.Prop.Fprop_mult_error]
mult_error_FLX_aux [in Flocq.Prop.Fprop_mult_error]


N

negb_Rle_bool [in Flocq.Core.Fcore_Raux]
negb_Rlt_bool [in Flocq.Core.Fcore_Raux]
negb_Zlt_bool [in Flocq.Core.Fcore_Zaux]
negb_Zle_bool [in Flocq.Core.Fcore_Zaux]
neq_Z2R [in Flocq.Core.Fcore_Raux]
new_location_odd_correct [in Flocq.Calc.Fcalc_bracket]
new_location_correct [in Flocq.Calc.Fcalc_bracket]
new_location_even_correct [in Flocq.Calc.Fcalc_bracket]


O

Only_DN_or_UP [in Flocq.Core.Fcore_rnd]
ordered_steps [in Flocq.Calc.Fcalc_bracket]


P

plus_error [in Flocq.Prop.Fprop_plus_error]
plus_error_aux [in Flocq.Prop.Fprop_plus_error]
pred_plus_ulp [in Flocq.Core.Fcore_ulp]
pred_ge_0 [in Flocq.Core.Fcore_ulp]
pred_ge_bpow [in Flocq.Core.Fcore_ulp]
pred_plus_ulp_1 [in Flocq.Core.Fcore_ulp]
pred_lt_id [in Flocq.Core.Fcore_ulp]
pred_plus_ulp_2 [in Flocq.Core.Fcore_ulp]
P2R_INR [in Flocq.Core.Fcore_Raux]


R

Rabs_gt_inv [in Flocq.Core.Fcore_Raux]
Rabs_le [in Flocq.Core.Fcore_Raux]
Rabs_lt [in Flocq.Core.Fcore_Raux]
Rabs_ge_inv [in Flocq.Core.Fcore_Raux]
Rabs_minus_le [in Flocq.Core.Fcore_Raux]
Rabs_ge [in Flocq.Core.Fcore_Raux]
Rabs_lt_inv [in Flocq.Core.Fcore_Raux]
Rabs_gt [in Flocq.Core.Fcore_Raux]
Rabs_eq_Rabs [in Flocq.Core.Fcore_Raux]
Rabs_le_inv [in Flocq.Core.Fcore_Raux]
radix_gt_0 [in Flocq.Core.Fcore_Zaux]
radix_val_inj [in Flocq.Core.Fcore_Zaux]
radix_pos [in Flocq.Core.Fcore_Raux]
radix_gt_1 [in Flocq.Core.Fcore_Zaux]
Rcompare_sym [in Flocq.Core.Fcore_Raux]
Rcompare_Z2R [in Flocq.Core.Fcore_Raux]
Rcompare_plus_r [in Flocq.Core.Fcore_Raux]
Rcompare_half_l [in Flocq.Core.Fcore_Raux]
Rcompare_ceil_floor_mid [in Flocq.Core.Fcore_generic_fmt]
Rcompare_Lt_inv [in Flocq.Core.Fcore_Raux]
Rcompare_floor_ceil_mid [in Flocq.Core.Fcore_generic_fmt]
Rcompare_Eq_inv [in Flocq.Core.Fcore_Raux]
Rcompare_spec [in Flocq.Core.Fcore_Raux]
Rcompare_Lt [in Flocq.Core.Fcore_Raux]
Rcompare_F2R [in Flocq.Core.Fcore_float_prop]
Rcompare_not_Lt [in Flocq.Core.Fcore_Raux]
Rcompare_Eq [in Flocq.Core.Fcore_Raux]
Rcompare_not_Lt_inv [in Flocq.Core.Fcore_Raux]
Rcompare_mult_l [in Flocq.Core.Fcore_Raux]
Rcompare_half_r [in Flocq.Core.Fcore_Raux]
Rcompare_Gt_inv [in Flocq.Core.Fcore_Raux]
Rcompare_not_Gt_inv [in Flocq.Core.Fcore_Raux]
Rcompare_plus_l [in Flocq.Core.Fcore_Raux]
Rcompare_Gt [in Flocq.Core.Fcore_Raux]
Rcompare_middle [in Flocq.Core.Fcore_Raux]
Rcompare_mult_r [in Flocq.Core.Fcore_Raux]
Rcompare_not_Gt [in Flocq.Core.Fcore_Raux]
Rcompare_sqr [in Flocq.Core.Fcore_Raux]
relative_error_N_FLX_ex [in Flocq.Prop.Fprop_relative]
relative_error_N_F2R_emin_ex [in Flocq.Prop.Fprop_relative]
relative_error_round_F2R_emin [in Flocq.Prop.Fprop_relative]
relative_error_round [in Flocq.Prop.Fprop_relative]
relative_error_N [in Flocq.Prop.Fprop_relative]
relative_error_FLT_F2R_emin [in Flocq.Prop.Fprop_relative]
relative_error_FLT_F2R_emin_ex [in Flocq.Prop.Fprop_relative]
relative_error_N_FLT_ex [in Flocq.Prop.Fprop_relative]
relative_error_N_ex [in Flocq.Prop.Fprop_relative]
relative_error_N_F2R_emin [in Flocq.Prop.Fprop_relative]
relative_error_N_FLT [in Flocq.Prop.Fprop_relative]
relative_error_le_conversion [in Flocq.Prop.Fprop_relative]
relative_error_FLX_round [in Flocq.Prop.Fprop_relative]
relative_error_N_FLT_round_F2R_emin [in Flocq.Prop.Fprop_relative]
relative_error_N_round [in Flocq.Prop.Fprop_relative]
relative_error_lt_conversion [in Flocq.Prop.Fprop_relative]
relative_error_FLT [in Flocq.Prop.Fprop_relative]
relative_error_N_round_F2R_emin [in Flocq.Prop.Fprop_relative]
relative_error_ex [in Flocq.Prop.Fprop_relative]
relative_error_N_FLX [in Flocq.Prop.Fprop_relative]
relative_error_N_FLT_round [in Flocq.Prop.Fprop_relative]
relative_error_F2R_emin_ex [in Flocq.Prop.Fprop_relative]
relative_error_FLX_ex [in Flocq.Prop.Fprop_relative]
relative_error_N_FLX_round [in Flocq.Prop.Fprop_relative]
relative_error_N_FLT_F2R_emin [in Flocq.Prop.Fprop_relative]
relative_error_F2R_emin [in Flocq.Prop.Fprop_relative]
relative_error [in Flocq.Prop.Fprop_relative]
relative_error_FLX_aux [in Flocq.Prop.Fprop_relative]
relative_error_FLX [in Flocq.Prop.Fprop_relative]
relative_error_FLT_ex [in Flocq.Prop.Fprop_relative]
relative_error_FLT_aux [in Flocq.Prop.Fprop_relative]
relative_error_N_FLT_F2R_emin_ex [in Flocq.Prop.Fprop_relative]
Req_bool_spec [in Flocq.Core.Fcore_Raux]
Req_bool_true [in Flocq.Core.Fcore_Raux]
Req_bool_false [in Flocq.Core.Fcore_Raux]
Rinv_lt [in Flocq.Core.Fcore_Raux]
Rinv_le [in Flocq.Core.Fcore_Raux]
Rle_0_minus [in Flocq.Core.Fcore_Raux]
Rle_bool_false [in Flocq.Core.Fcore_Raux]
Rle_bool_spec [in Flocq.Core.Fcore_Raux]
Rle_bool_true [in Flocq.Core.Fcore_Raux]
Rlt_bool_false [in Flocq.Core.Fcore_Raux]
Rlt_bool_spec [in Flocq.Core.Fcore_Raux]
Rlt_bool_true [in Flocq.Core.Fcore_Raux]
Rmin_compare [in Flocq.Core.Fcore_Raux]
Rmult_eq_reg_r [in Flocq.Core.Fcore_Raux]
Rmult_minus_distr_r [in Flocq.Core.Fcore_Raux]
Rmult_le_reg_r [in Flocq.Core.Fcore_Raux]
Rmult_min_distr_r [in Flocq.Core.Fcore_Raux]
Rmult_lt_reg_r [in Flocq.Core.Fcore_Raux]
Rmult_min_distr_l [in Flocq.Core.Fcore_Raux]
Rnd_DN_pt_idempotent [in Flocq.Core.Fcore_rnd]
Rnd_DN_UP_pt_N [in Flocq.Core.Fcore_rnd]
Rnd_NA_pt_monotone [in Flocq.Core.Fcore_rnd]
Rnd_NA_unicity [in Flocq.Core.Fcore_rnd]
Rnd_DN_pt_monotone [in Flocq.Core.Fcore_rnd]
Rnd_N_pt_refl [in Flocq.Core.Fcore_rnd]
Rnd_NG_pt_refl [in Flocq.Core.Fcore_rnd]
Rnd_ZR_abs [in Flocq.Core.Fcore_rnd]
Rnd_N_pt_0 [in Flocq.Core.Fcore_rnd]
Rnd_N_pt_DN_or_UP_eq [in Flocq.Core.Fcore_rnd]
Rnd_UP_pt_refl [in Flocq.Core.Fcore_rnd]
Rnd_DN_pt_equiv_format [in Flocq.Core.Fcore_rnd]
Rnd_DN_pt_unicity [in Flocq.Core.Fcore_rnd]
Rnd_UP_pt_unicity [in Flocq.Core.Fcore_rnd]
Rnd_NA_pt_refl [in Flocq.Core.Fcore_rnd]
Rnd_NG_pt_monotone [in Flocq.Core.Fcore_rnd]
Rnd_NE_pt_round [in Flocq.Core.Fcore_rnd_ne]
Rnd_NA_N_pt [in Flocq.Core.Fcore_rnd]
Rnd_N_pt_idempotent [in Flocq.Core.Fcore_rnd]
Rnd_N_pt_neg [in Flocq.Core.Fcore_rnd]
Rnd_ZR_pt_monotone [in Flocq.Core.Fcore_rnd]
Rnd_NG_pt_unicity [in Flocq.Core.Fcore_rnd]
Rnd_N_pt_DN_or_UP [in Flocq.Core.Fcore_rnd]
Rnd_NA_pt_unicity [in Flocq.Core.Fcore_rnd]
Rnd_N_pt_monotone [in Flocq.Core.Fcore_rnd]
Rnd_N_pt_sym [in Flocq.Core.Fcore_rnd]
Rnd_DN_pt_refl [in Flocq.Core.Fcore_rnd]
Rnd_N_pt_unicity [in Flocq.Core.Fcore_rnd]
Rnd_N_pt_pos [in Flocq.Core.Fcore_rnd]
Rnd_NG_unicity [in Flocq.Core.Fcore_rnd]
Rnd_NG_pt_sym [in Flocq.Core.Fcore_rnd]
Rnd_UP_pt_idempotent [in Flocq.Core.Fcore_rnd]
Rnd_DN_UP_sym [in Flocq.Core.Fcore_rnd]
Rnd_NA_NG_pt [in Flocq.Core.Fcore_rnd]
Rnd_NA_pt_unicity_prop [in Flocq.Core.Fcore_rnd]
Rnd_UP_DN_pt_sym [in Flocq.Core.Fcore_rnd]
Rnd_DN_unicity [in Flocq.Core.Fcore_rnd]
Rnd_NE_pt_monotone [in Flocq.Core.Fcore_rnd_ne]
Rnd_UP_pt_monotone [in Flocq.Core.Fcore_rnd]
Rnd_DN_pt_N [in Flocq.Core.Fcore_rnd]
Rnd_N_pt_abs [in Flocq.Core.Fcore_rnd]
Rnd_DN_UP_pt_split [in Flocq.Core.Fcore_rnd]
Rnd_NA_pt_idempotent [in Flocq.Core.Fcore_rnd]
Rnd_UP_pt_N [in Flocq.Core.Fcore_rnd]
Rnd_NE_pt_total [in Flocq.Core.Fcore_rnd_ne]
Rnd_UP_unicity [in Flocq.Core.Fcore_rnd]
Rnd_DN_UP_pt_sym [in Flocq.Core.Fcore_rnd]
Rnd_UP_pt_equiv_format [in Flocq.Core.Fcore_rnd]
round_UP_pt [in Flocq.Core.Fcore_generic_fmt]
round_sign_any_correct [in Flocq.Calc.Fcalc_round]
round_DN_pred [in Flocq.Core.Fcore_ulp]
round_UP_opp [in Flocq.Core.Fcore_generic_fmt]
round_ZR_pt [in Flocq.Core.Fcore_generic_fmt]
round_DN_succ [in Flocq.Core.Fcore_ulp]
round_generic [in Flocq.Core.Fcore_generic_fmt]
round_bounded_small_pos [in Flocq.Core.Fcore_generic_fmt]
round_UP_pred [in Flocq.Core.Fcore_ulp]
round_le_generic [in Flocq.Core.Fcore_generic_fmt]
round_trunc_sign_any_correct [in Flocq.Calc.Fcalc_round]
round_UP_succ [in Flocq.Core.Fcore_ulp]
round_N_pt [in Flocq.Core.Fcore_generic_fmt]
round_DN_pt [in Flocq.Core.Fcore_generic_fmt]
round_large_pos_ge_pow [in Flocq.Core.Fcore_generic_fmt]
round_abs_abs [in Flocq.Core.Fcore_generic_fmt]
round_opp [in Flocq.Core.Fcore_generic_fmt]
round_N_middle [in Flocq.Core.Fcore_generic_fmt]
round_NE_pt [in Flocq.Core.Fcore_rnd_ne]
round_ext [in Flocq.Core.Fcore_generic_fmt]
round_DN_or_UP [in Flocq.Core.Fcore_generic_fmt]
round_0 [in Flocq.Core.Fcore_generic_fmt]
round_pred_le_0 [in Flocq.Core.Fcore_rnd]
round_pred_lt_0 [in Flocq.Core.Fcore_rnd]
round_UP_small_pos [in Flocq.Core.Fcore_generic_fmt]
round_bounded_large_pos [in Flocq.Core.Fcore_generic_fmt]
round_N_opp [in Flocq.Core.Fcore_generic_fmt]
round_unicity [in Flocq.Core.Fcore_rnd]
round_NE_opp [in Flocq.Core.Fcore_rnd_ne]
round_NA_pt [in Flocq.Core.Fcore_generic_fmt]
round_NE_pt_pos [in Flocq.Core.Fcore_rnd_ne]
round_val_of_pred [in Flocq.Core.Fcore_rnd]
round_FTZ_FLX [in Flocq.Core.Fcore_FTZ]
round_FLT_FLX [in Flocq.Core.Fcore_FLT]
round_FTZ_small [in Flocq.Core.Fcore_FTZ]
round_pred_ge_0 [in Flocq.Core.Fcore_rnd]
round_plus_eq_zero [in Flocq.Prop.Fprop_plus_error]
round_le_pos [in Flocq.Core.Fcore_generic_fmt]
round_trunc_any_correct [in Flocq.Calc.Fcalc_round]
round_pred_gt_0 [in Flocq.Core.Fcore_rnd]
round_repr_same_exp [in Flocq.Prop.Fprop_plus_error]
round_le [in Flocq.Core.Fcore_generic_fmt]
round_ge_generic [in Flocq.Core.Fcore_generic_fmt]
round_fun_of_pred [in Flocq.Core.Fcore_rnd]
round_DN_small_pos [in Flocq.Core.Fcore_generic_fmt]
round_any_correct [in Flocq.Calc.Fcalc_round]
round_plus_eq_zero_aux [in Flocq.Prop.Fprop_plus_error]
round_DN_opp [in Flocq.Core.Fcore_generic_fmt]
Rplus_eq_reg_r [in Flocq.Core.Fcore_Raux]
Rplus_le_reg_r [in Flocq.Core.Fcore_Raux]


S

satisfies_any_imp_NA [in Flocq.Core.Fcore_rnd]
satisfies_any_imp_ZR [in Flocq.Core.Fcore_rnd]
satisfies_any_eq [in Flocq.Core.Fcore_rnd]
satisfies_any_imp_DN [in Flocq.Core.Fcore_rnd]
satisfies_any_imp_UP [in Flocq.Core.Fcore_rnd]
satisfies_any_imp_NG [in Flocq.Core.Fcore_rnd]
scaled_mantissa_mult_bpow [in Flocq.Core.Fcore_generic_fmt]
scaled_mantissa_abs [in Flocq.Core.Fcore_generic_fmt]
scaled_mantissa_small [in Flocq.Core.Fcore_generic_fmt]
scaled_mantissa_DN [in Flocq.Core.Fcore_generic_fmt]
scaled_mantissa_opp [in Flocq.Core.Fcore_generic_fmt]
scaled_mantissa_generic [in Flocq.Core.Fcore_generic_fmt]
scaled_mantissa_0 [in Flocq.Core.Fcore_generic_fmt]
shl_align_correct [in Flocq.Appli.Fappli_IEEE]
shl_align_fexp_correct [in Flocq.Appli.Fappli_IEEE]
shr_m_shr_record_of_loc [in Flocq.Appli.Fappli_IEEE]
shr_truncate [in Flocq.Appli.Fappli_IEEE]
snd_shl_align [in Flocq.Appli.Fappli_IEEE]
split_bits_of_binary_float_correct [in Flocq.Appli.Fappli_IEEE_bits]
split_join_bits [in Flocq.Appli.Fappli_IEEE_bits]
split_bits_inj [in Flocq.Appli.Fappli_IEEE_bits]
sqrt_error_FLX_N [in Flocq.Prop.Fprop_div_sqrt_error]
sqrt_ge_0 [in Flocq.Core.Fcore_Raux]
sterbenz [in Flocq.Prop.Fprop_Sterbenz]
sterbenz_aux [in Flocq.Prop.Fprop_Sterbenz]
subnormal_exponent [in Flocq.Core.Fcore_generic_fmt]
succ_le_lt [in Flocq.Core.Fcore_ulp]
succ_le_bpow [in Flocq.Core.Fcore_ulp]


T

truncate_0 [in Flocq.Calc.Fcalc_round]
truncate_aux_comp [in Flocq.Calc.Fcalc_round]
truncate_correct [in Flocq.Calc.Fcalc_round]
truncate_correct_partial [in Flocq.Calc.Fcalc_round]
truncate_correct_format [in Flocq.Calc.Fcalc_round]
truncate_FIX_correct [in Flocq.Calc.Fcalc_round]


U

ulp_half_error_f [in Flocq.Core.Fcore_ulp]
ulp_bpow [in Flocq.Core.Fcore_ulp]
ulp_abs [in Flocq.Core.Fcore_ulp]
ulp_half_error [in Flocq.Core.Fcore_ulp]
ulp_DN_UP [in Flocq.Core.Fcore_ulp]
ulp_error [in Flocq.Core.Fcore_ulp]
ulp_error_f [in Flocq.Core.Fcore_ulp]
ulp_le_id [in Flocq.Core.Fcore_ulp]
ulp_le [in Flocq.Core.Fcore_ulp]
ulp_le_abs [in Flocq.Core.Fcore_ulp]
ulp_opp [in Flocq.Core.Fcore_ulp]
ulp_DN [in Flocq.Core.Fcore_ulp]


V

valid_binary_B2FF [in Flocq.Appli.Fappli_IEEE]


Z

Zaway_abs [in Flocq.Core.Fcore_Raux]
Zaway_ceil [in Flocq.Core.Fcore_Raux]
Zaway_le [in Flocq.Core.Fcore_Raux]
Zaway_opp [in Flocq.Core.Fcore_Raux]
Zaway_floor [in Flocq.Core.Fcore_Raux]
Zaway_Z2R [in Flocq.Core.Fcore_Raux]
Zceil_Z2R [in Flocq.Core.Fcore_Raux]
Zceil_le [in Flocq.Core.Fcore_Raux]
Zceil_imp [in Flocq.Core.Fcore_Raux]
Zceil_ub [in Flocq.Core.Fcore_Raux]
Zceil_glb [in Flocq.Core.Fcore_Raux]
Zceil_floor_neq [in Flocq.Core.Fcore_Raux]
Zcompare_spec [in Flocq.Core.Fcore_Zaux]
Zcompare_Lt [in Flocq.Core.Fcore_Zaux]
Zcompare_Eq [in Flocq.Core.Fcore_Zaux]
Zcompare_Gt [in Flocq.Core.Fcore_Zaux]
Zdigits_mult_strong [in Flocq.Calc.Fcalc_digits]
Zdigits_ln_beta [in Flocq.Calc.Fcalc_digits]
Zdigits_Zpower [in Flocq.Calc.Fcalc_digits]
Zdigits_slice [in Flocq.Core.Fcore_digits]
Zdigits_correct [in Flocq.Core.Fcore_digits]
Zdigits_mult_Zpower [in Flocq.Calc.Fcalc_digits]
Zdigits_abs [in Flocq.Core.Fcore_digits]
Zdigits_ge_0 [in Flocq.Core.Fcore_digits]
Zdigits_gt_0 [in Flocq.Core.Fcore_digits]
Zdigits_gt_Zpower [in Flocq.Calc.Fcalc_digits]
Zdigits_mult [in Flocq.Calc.Fcalc_digits]
Zdigits_le_Zpower [in Flocq.Calc.Fcalc_digits]
Zdigits_le [in Flocq.Calc.Fcalc_digits]
Zdigits_div_Zpower [in Flocq.Calc.Fcalc_digits]
Zdigits_mult_ge [in Flocq.Calc.Fcalc_digits]
Zdigits2_Zdigits [in Flocq.Appli.Fappli_IEEE]
Zdigit_scale [in Flocq.Core.Fcore_digits]
Zdigit_mod_pow_out [in Flocq.Core.Fcore_digits]
Zdigit_mul_pow [in Flocq.Core.Fcore_digits]
Zdigit_not_0 [in Flocq.Core.Fcore_digits]
Zdigit_out [in Flocq.Core.Fcore_digits]
Zdigit_div_pow [in Flocq.Core.Fcore_digits]
Zdigit_slice_out [in Flocq.Core.Fcore_digits]
Zdigit_lt [in Flocq.Core.Fcore_digits]
Zdigit_mod_pow [in Flocq.Core.Fcore_digits]
Zdigit_0 [in Flocq.Core.Fcore_digits]
Zdigit_ge_Zpower_pos [in Flocq.Core.Fcore_digits]
Zdigit_slice [in Flocq.Core.Fcore_digits]
Zdigit_digits [in Flocq.Core.Fcore_digits]
Zdigit_ext [in Flocq.Core.Fcore_digits]
Zdigit_not_0_pos [in Flocq.Core.Fcore_digits]
Zdigit_opp [in Flocq.Core.Fcore_digits]
Zdigit_ge_Zpower [in Flocq.Core.Fcore_digits]
Zdigit_plus [in Flocq.Core.Fcore_digits]
Zdiv_mod_mult [in Flocq.Core.Fcore_Zaux]
Zeq_bool_false [in Flocq.Core.Fcore_Zaux]
Zeq_bool_true [in Flocq.Core.Fcore_Zaux]
Zeq_bool_spec [in Flocq.Core.Fcore_Zaux]
Zeven_Zpower_odd [in Flocq.Core.Fcore_Zaux]
Zeven_ex [in Flocq.Core.Fcore_Zaux]
Zeven_2xp1 [in Flocq.Core.Fcore_Zaux]
Zeven_mult [in Flocq.Core.Fcore_Zaux]
Zeven_opp [in Flocq.Core.Fcore_Zaux]
Zeven_Zpower [in Flocq.Core.Fcore_Zaux]
Zeven_plus [in Flocq.Core.Fcore_Zaux]
Zfloor_ub [in Flocq.Core.Fcore_Raux]
Zfloor_imp [in Flocq.Core.Fcore_Raux]
Zfloor_div [in Flocq.Core.Fcore_Raux]
Zfloor_lb [in Flocq.Core.Fcore_Raux]
Zfloor_lub [in Flocq.Core.Fcore_Raux]
Zfloor_le [in Flocq.Core.Fcore_Raux]
Zfloor_Z2R [in Flocq.Core.Fcore_Raux]
Zgt_not_eq [in Flocq.Core.Fcore_Zaux]
Zle_bool_false [in Flocq.Core.Fcore_Zaux]
Zle_bool_spec [in Flocq.Core.Fcore_Zaux]
Zle_bool_true [in Flocq.Core.Fcore_Zaux]
Zlt_bool_true [in Flocq.Core.Fcore_Zaux]
Zlt_bool_spec [in Flocq.Core.Fcore_Zaux]
Zlt_bool_false [in Flocq.Core.Fcore_Zaux]
Zmod_mod_mult [in Flocq.Core.Fcore_Zaux]
Znearest_ge_floor [in Flocq.Core.Fcore_generic_fmt]
Znearest_N [in Flocq.Core.Fcore_generic_fmt]
Znearest_opp [in Flocq.Core.Fcore_generic_fmt]
Znearest_le_ceil [in Flocq.Core.Fcore_generic_fmt]
Znearest_N_strict [in Flocq.Core.Fcore_generic_fmt]
Znearest_DN_or_UP [in Flocq.Core.Fcore_generic_fmt]
ZOdiv_small_abs [in Flocq.Core.Fcore_Zaux]
ZOdiv_plus [in Flocq.Core.Fcore_Zaux]
ZOdiv_plus_pow_digit [in Flocq.Core.Fcore_digits]
ZOdiv_mod_mult [in Flocq.Core.Fcore_Zaux]
ZOmod_eq [in Flocq.Core.Fcore_Zaux]
ZOmod_small_abs [in Flocq.Core.Fcore_Zaux]
ZOmod_plus_pow_digit [in Flocq.Core.Fcore_digits]
ZOmod_mod_mult [in Flocq.Core.Fcore_Zaux]
Zopp_le_cancel [in Flocq.Core.Fcore_Zaux]
Zplus_slice [in Flocq.Core.Fcore_digits]
Zpower_nat_S [in Flocq.Core.Fcore_Zaux]
Zpower_ge_0 [in Flocq.Core.Fcore_Zaux]
Zpower_lt_Zpower [in Flocq.Core.Fcore_Zaux]
Zpower_le_Zdigits [in Flocq.Calc.Fcalc_digits]
Zpower_pos_gt_0 [in Flocq.Core.Fcore_Zaux]
Zpower_gt_1 [in Flocq.Core.Fcore_Zaux]
Zpower_plus [in Flocq.Core.Fcore_Zaux]
Zpower_le [in Flocq.Core.Fcore_Zaux]
Zpower_lt [in Flocq.Core.Fcore_Zaux]
Zpower_Zpower_nat [in Flocq.Core.Fcore_Zaux]
Zpower_gt_id [in Flocq.Core.Fcore_digits]
Zpower_gt_0 [in Flocq.Core.Fcore_Zaux]
Zpower_gt_Zdigits [in Flocq.Calc.Fcalc_digits]
Zrnd_DN_or_UP [in Flocq.Core.Fcore_generic_fmt]
Zsame_sign_imp [in Flocq.Core.Fcore_Zaux]
Zsame_sign_scale [in Flocq.Core.Fcore_digits]
Zsame_sign_odiv [in Flocq.Core.Fcore_Zaux]
Zsame_sign_trans_weak [in Flocq.Core.Fcore_Zaux]
Zsame_sign_slice [in Flocq.Core.Fcore_digits]
Zsame_sign_trans [in Flocq.Core.Fcore_Zaux]
Zscale_0 [in Flocq.Core.Fcore_digits]
Zscale_scale [in Flocq.Core.Fcore_digits]
Zscale_mul_pow [in Flocq.Core.Fcore_digits]
Zslice_mul_pow [in Flocq.Core.Fcore_digits]
Zslice_slice [in Flocq.Core.Fcore_digits]
Zslice_div_pow_scale [in Flocq.Core.Fcore_digits]
Zslice_div_pow [in Flocq.Core.Fcore_digits]
Zslice_0 [in Flocq.Core.Fcore_digits]
Zslice_scale [in Flocq.Core.Fcore_digits]
Zsqrt_aux_correct [in Flocq.Calc.Fcalc_sqrt]
Zsqrt_ind [in Flocq.Calc.Fcalc_sqrt]
Zsqrt_correct [in Flocq.Calc.Fcalc_sqrt]
Zsum_digit_digit [in Flocq.Core.Fcore_digits]
Ztrunc_le [in Flocq.Core.Fcore_Raux]
Ztrunc_floor [in Flocq.Core.Fcore_Raux]
Ztrunc_ceil [in Flocq.Core.Fcore_Raux]
Ztrunc_opp [in Flocq.Core.Fcore_Raux]
Ztrunc_lub [in Flocq.Core.Fcore_Raux]
Ztrunc_Z2R [in Flocq.Core.Fcore_Raux]
Ztrunc_abs [in Flocq.Core.Fcore_Raux]
Z_of_nat_S_digits2_Pnat [in Flocq.Calc.Fcalc_digits]
Z2R_cond_Zopp [in Flocq.Core.Fcore_Raux]
Z2R_opp [in Flocq.Core.Fcore_Raux]
Z2R_Zpower [in Flocq.Core.Fcore_Raux]
Z2R_Zpower_nat [in Flocq.Core.Fcore_Raux]
Z2R_abs [in Flocq.Core.Fcore_Raux]
Z2R_neq [in Flocq.Core.Fcore_Raux]
Z2R_Zpower_pos [in Flocq.Core.Fcore_Raux]
Z2R_minus [in Flocq.Core.Fcore_Raux]
Z2R_mult [in Flocq.Core.Fcore_Raux]
Z2R_plus [in Flocq.Core.Fcore_Raux]
Z2R_le [in Flocq.Core.Fcore_Raux]
Z2R_lt [in Flocq.Core.Fcore_Raux]
Z2R_IZR [in Flocq.Core.Fcore_Raux]
Z2R_le_lt [in Flocq.Core.Fcore_Raux]



Section Index

A

AnyRadix [in Flocq.Appli.Fappli_IEEE]


B

Binary [in Flocq.Appli.Fappli_IEEE]
Binary_Bits [in Flocq.Appli.Fappli_IEEE_bits]
Bool [in Flocq.Core.Fcore_Raux]
B32_Bits [in Flocq.Appli.Fappli_IEEE_bits]
B64_Bits [in Flocq.Appli.Fappli_IEEE_bits]


C

cond_opp [in Flocq.Core.Fcore_Raux]


D

Def [in Flocq.Core.Fcore_defs]
Div_Mod [in Flocq.Core.Fcore_Zaux]


E

Even_Odd [in Flocq.Core.Fcore_Zaux]


F

Fcalc_bracket.Fcalc_bracket_any [in Flocq.Calc.Fcalc_bracket]
Fcalc_round.Fcalc_round_fexp.round_dir [in Flocq.Calc.Fcalc_round]
Fcalc_bracket_scale [in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket [in Flocq.Calc.Fcalc_bracket]
Fcalc_div [in Flocq.Calc.Fcalc_div]
Fcalc_sqrt [in Flocq.Calc.Fcalc_sqrt]
Fcalc_bracket_step [in Flocq.Calc.Fcalc_bracket]
Fcalc_round.Fcalc_round_fexp [in Flocq.Calc.Fcalc_round]
Fcalc_round.Fcalc_round_fexp.round_dir_sign [in Flocq.Calc.Fcalc_round]
Fcalc_round [in Flocq.Calc.Fcalc_round]
Fcalc_bracket_generic [in Flocq.Calc.Fcalc_bracket]
Fcalc_digits [in Flocq.Calc.Fcalc_digits]
Fcore_ulp [in Flocq.Core.Fcore_ulp]
Fcore_rnd_NE [in Flocq.Core.Fcore_rnd_ne]
Fcore_digits.digits_aux [in Flocq.Core.Fcore_digits]
Fcore_digits [in Flocq.Core.Fcore_digits]
Float_prop [in Flocq.Core.Fcore_float_prop]
Float_ops [in Flocq.Calc.Fcalc_ops]
Floor_Ceil [in Flocq.Core.Fcore_Raux]
Fprop_plus_zero [in Flocq.Prop.Fprop_plus_error]
Fprop_relative.Fprop_relative_FLT [in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_FLX [in Flocq.Prop.Fprop_relative]
Fprop_mult_error [in Flocq.Prop.Fprop_mult_error]
Fprop_Sterbenz [in Flocq.Prop.Fprop_Sterbenz]
Fprop_relative.Fprop_relative_generic [in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_generic.relative_error_conversion [in Flocq.Prop.Fprop_relative]
Fprop_plus_zero.round_plus_eq_zero_aux [in Flocq.Prop.Fprop_plus_error]
Fprop_plus_error [in Flocq.Prop.Fprop_plus_error]
Fprop_relative [in Flocq.Prop.Fprop_relative]
Fprop_plus_error.round_repr_same_exp [in Flocq.Prop.Fprop_plus_error]
Fprop_divsqrt_error [in Flocq.Prop.Fprop_div_sqrt_error]
Fprop_mult_error_FLT [in Flocq.Prop.Fprop_mult_error]


G

Generic [in Flocq.Core.Fcore_generic_fmt]
Generic.Format [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.Fcore_generic_round_pos [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.monotone [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.monotone_abs [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.monotone_exp [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.not_FTZ [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.rndNA [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.rndN_opp [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.round_large [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.Znearest [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.Zround_opp [in Flocq.Core.Fcore_generic_fmt]
Generic.Inclusion [in Flocq.Core.Fcore_generic_fmt]


P

pow [in Flocq.Core.Fcore_Raux]
Proof_Irrelevance [in Flocq.Core.Fcore_Zaux]


R

Rcompare [in Flocq.Core.Fcore_Raux]
Req_bool [in Flocq.Core.Fcore_Raux]
Rle_bool [in Flocq.Core.Fcore_Raux]
Rlt_bool [in Flocq.Core.Fcore_Raux]
Rmissing [in Flocq.Core.Fcore_Raux]
RND [in Flocq.Core.Fcore_defs]
RND_prop [in Flocq.Core.Fcore_rnd]
RND_FIX [in Flocq.Core.Fcore_FIX]
RND_FLX [in Flocq.Core.Fcore_FLX]
RND_FTZ.FTZ_round [in Flocq.Core.Fcore_FTZ]
RND_FTZ [in Flocq.Core.Fcore_FTZ]
RND_FLT [in Flocq.Core.Fcore_FLT]


S

Same_sign [in Flocq.Core.Fcore_Zaux]


Z

Zcompare [in Flocq.Core.Fcore_Zaux]
Zdiv_Rdiv [in Flocq.Core.Fcore_Raux]
Zeq_bool [in Flocq.Core.Fcore_Zaux]
Zle_bool [in Flocq.Core.Fcore_Zaux]
Zlt_bool [in Flocq.Core.Fcore_Zaux]
Zmissing [in Flocq.Core.Fcore_Zaux]
Zpower [in Flocq.Core.Fcore_Zaux]
Z2R [in Flocq.Core.Fcore_Raux]



Constructor Index

B

B754_nan [in Flocq.Appli.Fappli_IEEE]
B754_infinity [in Flocq.Appli.Fappli_IEEE]
B754_finite [in Flocq.Appli.Fappli_IEEE]
B754_zero [in Flocq.Appli.Fappli_IEEE]


E

exists_NE [in Flocq.Core.Fcore_rnd_ne]
exp_not_FTZ [in Flocq.Core.Fcore_generic_fmt]


F

Float [in Flocq.Core.Fcore_defs]
F754_zero [in Flocq.Appli.Fappli_IEEE]
F754_finite [in Flocq.Appli.Fappli_IEEE]
F754_infinity [in Flocq.Appli.Fappli_IEEE]
F754_nan [in Flocq.Appli.Fappli_IEEE]


I

inbetween_Inexact [in Flocq.Calc.Fcalc_bracket]
inbetween_Exact [in Flocq.Calc.Fcalc_bracket]


L

loc_Inexact [in Flocq.Calc.Fcalc_bracket]
loc_Exact [in Flocq.Calc.Fcalc_bracket]


M

mode_NA [in Flocq.Appli.Fappli_IEEE]
mode_DN [in Flocq.Appli.Fappli_IEEE]
mode_UP [in Flocq.Appli.Fappli_IEEE]
mode_ZR [in Flocq.Appli.Fappli_IEEE]
mode_NE [in Flocq.Appli.Fappli_IEEE]
monotone_exp [in Flocq.Core.Fcore_generic_fmt]


P

prec_gt_0 [in Flocq.Core.Fcore_FLX]


R

Rcompare_Lt_ [in Flocq.Core.Fcore_Raux]
Rcompare_Eq_ [in Flocq.Core.Fcore_Raux]
Rcompare_Gt_ [in Flocq.Core.Fcore_Raux]
Req_bool_false_ [in Flocq.Core.Fcore_Raux]
Req_bool_true_ [in Flocq.Core.Fcore_Raux]
Rle_bool_false_ [in Flocq.Core.Fcore_Raux]
Rle_bool_true_ [in Flocq.Core.Fcore_Raux]
Rlt_bool_false_ [in Flocq.Core.Fcore_Raux]
Rlt_bool_true_ [in Flocq.Core.Fcore_Raux]


S

Satisfies_any [in Flocq.Core.Fcore_rnd]


V

valid_exp [in Flocq.Core.Fcore_generic_fmt]


Z

Zcompare_Lt_ [in Flocq.Core.Fcore_Zaux]
Zcompare_Eq_ [in Flocq.Core.Fcore_Zaux]
Zcompare_Gt_ [in Flocq.Core.Fcore_Zaux]
Zeq_bool_true_ [in Flocq.Core.Fcore_Zaux]
Zeq_bool_false_ [in Flocq.Core.Fcore_Zaux]
Zle_bool_false_ [in Flocq.Core.Fcore_Zaux]
Zle_bool_true_ [in Flocq.Core.Fcore_Zaux]
Zlt_bool_true_ [in Flocq.Core.Fcore_Zaux]
Zlt_bool_false_ [in Flocq.Core.Fcore_Zaux]



Abbreviation Index

B

bpow [in Flocq.Prop.Fprop_div_sqrt_error]
bpow [in Flocq.Prop.Fprop_plus_error]
bpow [in Flocq.Core.Fcore_rnd_ne]
bpow [in Flocq.Prop.Fprop_relative]
bpow [in Flocq.Prop.Fprop_mult_error]
bpow [in Flocq.Core.Fcore_ulp]
bpow [in Flocq.Core.Fcore_float_prop]
bpow [in Flocq.Core.Fcore_FLT]
bpow [in Flocq.Calc.Fcalc_bracket]
bpow [in Flocq.Prop.Fprop_plus_error]
bpow [in Flocq.Prop.Fprop_Sterbenz]
bpow [in Flocq.Core.Fcore_FLX]
bpow [in Flocq.Calc.Fcalc_ops]
bpow [in Flocq.Core.Fcore_generic_fmt]
bpow [in Flocq.Core.Fcore_FIX]
bpow [in Flocq.Calc.Fcalc_sqrt]
bpow [in Flocq.Core.Fcore_FTZ]
bpow [in Flocq.Calc.Fcalc_round]
bpow [in Flocq.Prop.Fprop_mult_error]
bpow [in Flocq.Calc.Fcalc_div]
bpow [in Flocq.Calc.Fcalc_digits]


C

canonic [in Flocq.Core.Fcore_rnd_ne]
cexp [in Flocq.Prop.Fprop_mult_error]
cexp [in Flocq.Prop.Fprop_mult_error]
cexp [in Flocq.Prop.Fprop_div_sqrt_error]


F

F [in Flocq.Core.Fcore_ulp]
format [in Flocq.Prop.Fprop_plus_error]
format [in Flocq.Calc.Fcalc_round]
format [in Flocq.Prop.Fprop_Sterbenz]
format [in Flocq.Prop.Fprop_plus_error]
format [in Flocq.Core.Fcore_rnd_ne]
format [in Flocq.Prop.Fprop_mult_error]
format [in Flocq.Prop.Fprop_div_sqrt_error]
format [in Flocq.Prop.Fprop_mult_error]


R

rndDN [in Flocq.Core.Fcore_generic_fmt]
rndNA [in Flocq.Core.Fcore_generic_fmt]
rndNE [in Flocq.Core.Fcore_rnd_ne]
rndUP [in Flocq.Core.Fcore_generic_fmt]
rndZR [in Flocq.Core.Fcore_generic_fmt]


Z

ZnearestA [in Flocq.Core.Fcore_generic_fmt]
ZnearestE [in Flocq.Core.Fcore_rnd_ne]



Inductive Index

B

binary_float [in Flocq.Appli.Fappli_IEEE]


E

Exists_NE [in Flocq.Core.Fcore_rnd_ne]
Exp_not_FTZ [in Flocq.Core.Fcore_generic_fmt]


F

full_float [in Flocq.Appli.Fappli_IEEE]


I

inbetween [in Flocq.Calc.Fcalc_bracket]


L

location [in Flocq.Calc.Fcalc_bracket]


M

mode [in Flocq.Appli.Fappli_IEEE]
Monotone_exp [in Flocq.Core.Fcore_generic_fmt]


P

Prec_gt_0 [in Flocq.Core.Fcore_FLX]


R

Rcompare_prop [in Flocq.Core.Fcore_Raux]
Req_bool_prop [in Flocq.Core.Fcore_Raux]
Rle_bool_prop [in Flocq.Core.Fcore_Raux]
Rlt_bool_prop [in Flocq.Core.Fcore_Raux]


S

satisfies_any [in Flocq.Core.Fcore_rnd]


V

Valid_exp [in Flocq.Core.Fcore_generic_fmt]


Z

Zcompare_prop [in Flocq.Core.Fcore_Zaux]
Zeq_bool_prop [in Flocq.Core.Fcore_Zaux]
Zle_bool_prop [in Flocq.Core.Fcore_Zaux]
Zlt_bool_prop [in Flocq.Core.Fcore_Zaux]



Definition Index

B

Bdiv [in Flocq.Appli.Fappli_IEEE]
binary_normalize [in Flocq.Appli.Fappli_IEEE]
binary_round [in Flocq.Appli.Fappli_IEEE]
binary_float_of_bits_aux [in Flocq.Appli.Fappli_IEEE_bits]
binary_round_aux [in Flocq.Appli.Fappli_IEEE]
binary_overflow [in Flocq.Appli.Fappli_IEEE]
binary_float_of_bits [in Flocq.Appli.Fappli_IEEE_bits]
binary32 [in Flocq.Appli.Fappli_IEEE_bits]
binary64 [in Flocq.Appli.Fappli_IEEE_bits]
bits_of_binary_float [in Flocq.Appli.Fappli_IEEE_bits]
bits_of_b32 [in Flocq.Appli.Fappli_IEEE_bits]
bits_of_b64 [in Flocq.Appli.Fappli_IEEE_bits]
Bminus [in Flocq.Appli.Fappli_IEEE]
Bmult [in Flocq.Appli.Fappli_IEEE]
Bmult_FF [in Flocq.Appli.Fappli_IEEE]
Bopp [in Flocq.Appli.Fappli_IEEE]
bounded [in Flocq.Appli.Fappli_IEEE]
Bplus [in Flocq.Appli.Fappli_IEEE]
bpow [in Flocq.Core.Fcore_Raux]
Bsign [in Flocq.Appli.Fappli_IEEE]
Bsqrt [in Flocq.Appli.Fappli_IEEE]
B2FF [in Flocq.Appli.Fappli_IEEE]
B2R [in Flocq.Appli.Fappli_IEEE]
b32_mult [in Flocq.Appli.Fappli_IEEE_bits]
b32_opp [in Flocq.Appli.Fappli_IEEE_bits]
b32_div [in Flocq.Appli.Fappli_IEEE_bits]
b32_plus [in Flocq.Appli.Fappli_IEEE_bits]
b32_of_bits [in Flocq.Appli.Fappli_IEEE_bits]
b32_sqrt [in Flocq.Appli.Fappli_IEEE_bits]
b32_minus [in Flocq.Appli.Fappli_IEEE_bits]
b64_div [in Flocq.Appli.Fappli_IEEE_bits]
b64_plus [in Flocq.Appli.Fappli_IEEE_bits]
b64_of_bits [in Flocq.Appli.Fappli_IEEE_bits]
b64_opp [in Flocq.Appli.Fappli_IEEE_bits]
b64_sqrt [in Flocq.Appli.Fappli_IEEE_bits]
b64_minus [in Flocq.Appli.Fappli_IEEE_bits]
b64_mult [in Flocq.Appli.Fappli_IEEE_bits]


C

canonic [in Flocq.Core.Fcore_generic_fmt]
canonic_exp [in Flocq.Core.Fcore_generic_fmt]
canonic_mantissa [in Flocq.Appli.Fappli_IEEE]
choice_mode [in Flocq.Appli.Fappli_IEEE]
cond_Ropp [in Flocq.Core.Fcore_Raux]
cond_Zopp [in Flocq.Core.Fcore_Raux]
cond_incr [in Flocq.Calc.Fcalc_round]


D

digits2_Pnat [in Flocq.Core.Fcore_digits]
DN_UP_parity_prop [in Flocq.Core.Fcore_rnd_ne]
DN_UP_parity_pos_prop [in Flocq.Core.Fcore_rnd_ne]


E

eqbool_dep [in Flocq.Core.Fcore_Zaux]


F

Fabs [in Flocq.Calc.Fcalc_ops]
Falign [in Flocq.Calc.Fcalc_ops]
Fdiv_core_binary [in Flocq.Appli.Fappli_IEEE]
Fdiv_core [in Flocq.Calc.Fcalc_div]
FF2B [in Flocq.Appli.Fappli_IEEE]
FF2R [in Flocq.Appli.Fappli_IEEE]
FIX_exp [in Flocq.Core.Fcore_FIX]
FIX_format [in Flocq.Core.Fcore_FIX]
Flocq_version [in Flocq.Flocq_version]
FLT_exp [in Flocq.Core.Fcore_FLT]
FLT_format [in Flocq.Core.Fcore_FLT]
FLXN_format [in Flocq.Core.Fcore_FLX]
FLX_exp [in Flocq.Core.Fcore_FLX]
FLX_format [in Flocq.Core.Fcore_FLX]
Fminus [in Flocq.Calc.Fcalc_ops]
Fmult [in Flocq.Calc.Fcalc_ops]
Fopp [in Flocq.Calc.Fcalc_ops]
Fplus [in Flocq.Calc.Fcalc_ops]
Fsqrt_core [in Flocq.Calc.Fcalc_sqrt]
Fsqrt_core_binary [in Flocq.Appli.Fappli_IEEE]
FTZ_format [in Flocq.Core.Fcore_FTZ]
FTZ_exp [in Flocq.Core.Fcore_FTZ]
F2R [in Flocq.Core.Fcore_defs]


G

generic_format [in Flocq.Core.Fcore_generic_fmt]


I

inbetween_int [in Flocq.Calc.Fcalc_bracket]
inbetween_float [in Flocq.Calc.Fcalc_bracket]
inbetween_loc [in Flocq.Calc.Fcalc_bracket]
is_finite [in Flocq.Appli.Fappli_IEEE]
is_finite_FF [in Flocq.Appli.Fappli_IEEE]
is_finite_strict [in Flocq.Appli.Fappli_IEEE]


J

join_bits [in Flocq.Appli.Fappli_IEEE_bits]


L

ln_beta [in Flocq.Core.Fcore_Raux]
loc_of_shr_record [in Flocq.Appli.Fappli_IEEE]


N

new_location_odd [in Flocq.Calc.Fcalc_bracket]
new_location [in Flocq.Calc.Fcalc_bracket]
new_location_even [in Flocq.Calc.Fcalc_bracket]
NE_prop [in Flocq.Core.Fcore_rnd_ne]
NG_existence_prop [in Flocq.Core.Fcore_rnd]


O

overflow_to_inf [in Flocq.Appli.Fappli_IEEE]


P

pred [in Flocq.Core.Fcore_ulp]
P2R [in Flocq.Core.Fcore_Raux]


R

radix2 [in Flocq.Appli.Fappli_IEEE]
radix2 [in Flocq.Calc.Fcalc_digits]
Rcompare [in Flocq.Core.Fcore_Raux]
Req_bool [in Flocq.Core.Fcore_Raux]
Rle_bool [in Flocq.Core.Fcore_Raux]
Rlt_bool [in Flocq.Core.Fcore_Raux]
Rnd_ZR_pt [in Flocq.Core.Fcore_defs]
Rnd_ZR [in Flocq.Core.Fcore_defs]
Rnd_NA [in Flocq.Core.Fcore_defs]
Rnd_NA_pt [in Flocq.Core.Fcore_defs]
Rnd_N [in Flocq.Core.Fcore_defs]
Rnd_UP_pt [in Flocq.Core.Fcore_defs]
Rnd_DN_pt [in Flocq.Core.Fcore_defs]
Rnd_NG_pt_unicity_prop [in Flocq.Core.Fcore_rnd]
Rnd_NG [in Flocq.Core.Fcore_defs]
Rnd_NE_pt [in Flocq.Core.Fcore_rnd_ne]
Rnd_UP [in Flocq.Core.Fcore_defs]
Rnd_NG_pt [in Flocq.Core.Fcore_defs]
Rnd_N_pt [in Flocq.Core.Fcore_defs]
Rnd_DN [in Flocq.Core.Fcore_defs]
round [in Flocq.Core.Fcore_generic_fmt]
round_trunc_NA_correct [in Flocq.Calc.Fcalc_round]
round_pred_total [in Flocq.Core.Fcore_defs]
round_sign_NA_correct [in Flocq.Calc.Fcalc_round]
round_pred [in Flocq.Core.Fcore_defs]
round_trunc_sign_NA_correct [in Flocq.Calc.Fcalc_round]
round_trunc_sign_DN_correct [in Flocq.Calc.Fcalc_round]
round_sign_DN_correct [in Flocq.Calc.Fcalc_round]
round_UP [in Flocq.Calc.Fcalc_round]
round_sign_UP [in Flocq.Calc.Fcalc_round]
round_mode [in Flocq.Appli.Fappli_IEEE]
round_trunc_sign_NE_correct [in Flocq.Calc.Fcalc_round]
round_pred_monotone [in Flocq.Core.Fcore_defs]
round_UP_correct [in Flocq.Calc.Fcalc_round]
round_NA_correct [in Flocq.Calc.Fcalc_round]
round_NE_correct [in Flocq.Calc.Fcalc_round]
round_ZR_correct [in Flocq.Calc.Fcalc_round]
round_trunc_UP_correct [in Flocq.Calc.Fcalc_round]
round_N [in Flocq.Calc.Fcalc_round]
round_sign_ZR_correct [in Flocq.Calc.Fcalc_round]
round_sign_NE_correct [in Flocq.Calc.Fcalc_round]
round_ZR [in Flocq.Calc.Fcalc_round]
round_trunc_DN_correct [in Flocq.Calc.Fcalc_round]
round_trunc_sign_ZR_correct [in Flocq.Calc.Fcalc_round]
round_trunc_NE_correct [in Flocq.Calc.Fcalc_round]
round_sign_DN [in Flocq.Calc.Fcalc_round]
round_DN_correct [in Flocq.Calc.Fcalc_round]
round_trunc_ZR_correct [in Flocq.Calc.Fcalc_round]
round_trunc_sign_UP_correct [in Flocq.Calc.Fcalc_round]
round_sign_UP_correct [in Flocq.Calc.Fcalc_round]


S

scaled_mantissa [in Flocq.Core.Fcore_generic_fmt]
shl_align [in Flocq.Appli.Fappli_IEEE]
shl_align_fexp [in Flocq.Appli.Fappli_IEEE]
shr [in Flocq.Appli.Fappli_IEEE]
shr_1 [in Flocq.Appli.Fappli_IEEE]
shr_record_of_loc [in Flocq.Appli.Fappli_IEEE]
shr_fexp [in Flocq.Appli.Fappli_IEEE]
sign_FF [in Flocq.Appli.Fappli_IEEE]
split_bits_of_binary_float [in Flocq.Appli.Fappli_IEEE_bits]
split_bits [in Flocq.Appli.Fappli_IEEE_bits]


T

truncate [in Flocq.Calc.Fcalc_round]
truncate_FIX [in Flocq.Calc.Fcalc_round]
truncate_aux [in Flocq.Calc.Fcalc_round]


U

ulp [in Flocq.Core.Fcore_ulp]


V

valid_binary [in Flocq.Appli.Fappli_IEEE]


Z

Zaway [in Flocq.Core.Fcore_Raux]
Zceil [in Flocq.Core.Fcore_Raux]
Zdigit [in Flocq.Core.Fcore_digits]
Zdigits [in Flocq.Core.Fcore_digits]
Zdigits_aux [in Flocq.Core.Fcore_digits]
Zdigits2 [in Flocq.Appli.Fappli_IEEE]
Zeven [in Flocq.Core.Fcore_Zaux]
Zfloor [in Flocq.Core.Fcore_Raux]
Znearest [in Flocq.Core.Fcore_generic_fmt]
Zrnd_FTZ [in Flocq.Core.Fcore_FTZ]
Zrnd_opp [in Flocq.Core.Fcore_generic_fmt]
Zscale [in Flocq.Core.Fcore_digits]
Zslice [in Flocq.Core.Fcore_digits]
Zsqrt [in Flocq.Calc.Fcalc_sqrt]
Zsqrt_aux [in Flocq.Calc.Fcalc_sqrt]
Zsum_digit [in Flocq.Core.Fcore_digits]
Ztrunc [in Flocq.Core.Fcore_Raux]
Z2R [in Flocq.Core.Fcore_Raux]



Variable Index

B

Binary_Bits.prec [in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.Hmax [in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.Hew [in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.ew [in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.emax [in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.emin [in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.Hprec [in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.Hmw [in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.Hm_gt_0 [in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.mw [in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.He_gt_0 [in Flocq.Appli.Fappli_IEEE_bits]
Binary_Bits.binary_float [in Flocq.Appli.Fappli_IEEE_bits]
Binary.emax [in Flocq.Appli.Fappli_IEEE]
Binary.emin [in Flocq.Appli.Fappli_IEEE]
Binary.fexp [in Flocq.Appli.Fappli_IEEE]
Binary.Hmax [in Flocq.Appli.Fappli_IEEE]
Binary.prec [in Flocq.Appli.Fappli_IEEE]
B32_Bits.Hprec [in Flocq.Appli.Fappli_IEEE_bits]
B32_Bits.Hprec_emax [in Flocq.Appli.Fappli_IEEE_bits]
B64_Bits.Hprec [in Flocq.Appli.Fappli_IEEE_bits]
B64_Bits.Hprec_emax [in Flocq.Appli.Fappli_IEEE_bits]


D

Def.beta [in Flocq.Core.Fcore_defs]


F

Fcalc_digits.beta [in Flocq.Calc.Fcalc_digits]
Fcalc_bracket.u [in Flocq.Calc.Fcalc_bracket]
Fcalc_round.Fcalc_round_fexp.round_dir_sign.choice [in Flocq.Calc.Fcalc_round]
Fcalc_bracket_step.Hnb_steps [in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket_step.start [in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket_step.step [in Flocq.Calc.Fcalc_bracket]
Fcalc_round.emin [in Flocq.Calc.Fcalc_round]
Fcalc_bracket_step.Hstep [in Flocq.Calc.Fcalc_bracket]
Fcalc_round.Fcalc_round_fexp.round_dir.rnd [in Flocq.Calc.Fcalc_round]
Fcalc_round.Fcalc_round_fexp.round_dir_sign.inbetween_int_valid [in Flocq.Calc.Fcalc_round]
Fcalc_round.Fcalc_round_fexp.round_dir.inbetween_int_valid [in Flocq.Calc.Fcalc_round]
Fcalc_bracket.x [in Flocq.Calc.Fcalc_bracket]
Fcalc_round.Fcalc_round_fexp.round_dir_sign.rnd [in Flocq.Calc.Fcalc_round]
Fcalc_round.Fcalc_round_fexp.fexp [in Flocq.Calc.Fcalc_round]
Fcalc_bracket.Hdu [in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket_step.nb_steps [in Flocq.Calc.Fcalc_bracket]
Fcalc_div.beta [in Flocq.Calc.Fcalc_div]
Fcalc_bracket.d [in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket.Fcalc_bracket_any.l [in Flocq.Calc.Fcalc_bracket]
Fcalc_bracket_generic.beta [in Flocq.Calc.Fcalc_bracket]
Fcalc_round.beta [in Flocq.Calc.Fcalc_round]
Fcalc_sqrt.beta [in Flocq.Calc.Fcalc_sqrt]
Fcalc_round.Fcalc_round_fexp.round_dir.choice [in Flocq.Calc.Fcalc_round]
Fcore_rnd_NE.beta [in Flocq.Core.Fcore_rnd_ne]
Fcore_ulp.fexp [in Flocq.Core.Fcore_ulp]
Fcore_digits.digits_aux.Hp [in Flocq.Core.Fcore_digits]
Fcore_rnd_NE.fexp [in Flocq.Core.Fcore_rnd_ne]
Fcore_ulp.beta [in Flocq.Core.Fcore_ulp]
Fcore_digits.beta [in Flocq.Core.Fcore_digits]
Fcore_digits.digits_aux.p [in Flocq.Core.Fcore_digits]
Float_ops.beta [in Flocq.Calc.Fcalc_ops]
Float_prop.beta [in Flocq.Core.Fcore_float_prop]
Fprop_relative.Fprop_relative_FLT.prec [in Flocq.Prop.Fprop_relative]
Fprop_plus_zero.round_plus_eq_zero_aux.rnd [in Flocq.Prop.Fprop_plus_error]
Fprop_mult_error.rnd [in Flocq.Prop.Fprop_mult_error]
Fprop_relative.Fprop_relative_FLT.rnd [in Flocq.Prop.Fprop_relative]
Fprop_relative.beta [in Flocq.Prop.Fprop_relative]
Fprop_mult_error_FLT.rnd [in Flocq.Prop.Fprop_mult_error]
Fprop_mult_error_FLT.Hpemin [in Flocq.Prop.Fprop_mult_error]
Fprop_mult_error_FLT.emin [in Flocq.Prop.Fprop_mult_error]
Fprop_relative.Fprop_relative_generic.p [in Flocq.Prop.Fprop_relative]
Fprop_mult_error_FLT.prec [in Flocq.Prop.Fprop_mult_error]
Fprop_mult_error_FLT.beta [in Flocq.Prop.Fprop_mult_error]
Fprop_relative.Fprop_relative_FLT.emin [in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_FLX.choice [in Flocq.Prop.Fprop_relative]
Fprop_divsqrt_error.prec [in Flocq.Prop.Fprop_div_sqrt_error]
Fprop_divsqrt_error.Hp1 [in Flocq.Prop.Fprop_div_sqrt_error]
Fprop_mult_error.beta [in Flocq.Prop.Fprop_mult_error]
Fprop_Sterbenz.fexp [in Flocq.Prop.Fprop_Sterbenz]
Fprop_plus_zero.fexp [in Flocq.Prop.Fprop_plus_error]
Fprop_plus_error.fexp [in Flocq.Prop.Fprop_plus_error]
Fprop_relative.Fprop_relative_generic.emin [in Flocq.Prop.Fprop_relative]
Fprop_plus_zero.beta [in Flocq.Prop.Fprop_plus_error]
Fprop_plus_error.choice [in Flocq.Prop.Fprop_plus_error]
Fprop_plus_error.beta [in Flocq.Prop.Fprop_plus_error]
Fprop_relative.Fprop_relative_generic.Hmin [in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_generic.rnd [in Flocq.Prop.Fprop_relative]
Fprop_plus_zero.rnd [in Flocq.Prop.Fprop_plus_error]
Fprop_relative.Fprop_relative_FLX.Hp [in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_FLT.Hp [in Flocq.Prop.Fprop_relative]
Fprop_plus_error.round_repr_same_exp.rnd [in Flocq.Prop.Fprop_plus_error]
Fprop_Sterbenz.beta [in Flocq.Prop.Fprop_Sterbenz]
Fprop_divsqrt_error.beta [in Flocq.Prop.Fprop_div_sqrt_error]
Fprop_relative.Fprop_relative_generic.fexp [in Flocq.Prop.Fprop_relative]
Fprop_divsqrt_error.choice [in Flocq.Prop.Fprop_div_sqrt_error]
Fprop_relative.Fprop_relative_generic.choice [in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_FLX.rnd [in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_FLT.choice [in Flocq.Prop.Fprop_relative]
Fprop_relative.Fprop_relative_generic.relative_error_conversion.rnd [in Flocq.Prop.Fprop_relative]
Fprop_mult_error.prec [in Flocq.Prop.Fprop_mult_error]
Fprop_relative.Fprop_relative_FLX.prec [in Flocq.Prop.Fprop_relative]


G

Generic.beta [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.Fcore_generic_round_pos.rnd [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.fexp [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.monotone_exp.rnd [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.monotone_abs.rnd [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.monotone.rnd [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.round_large.rnd [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.Znearest.choice [in Flocq.Core.Fcore_generic_fmt]
Generic.Format.Zround_opp.rnd [in Flocq.Core.Fcore_generic_fmt]
Generic.Inclusion.fexp1 [in Flocq.Core.Fcore_generic_fmt]
Generic.Inclusion.fexp2 [in Flocq.Core.Fcore_generic_fmt]


P

pow.r [in Flocq.Core.Fcore_Raux]


R

RND_FIX.beta [in Flocq.Core.Fcore_FIX]
RND_FLT.NE_prop [in Flocq.Core.Fcore_FLT]
RND_FLT.emin [in Flocq.Core.Fcore_FLT]
RND_FIX.emin [in Flocq.Core.Fcore_FIX]
RND_FLX.beta [in Flocq.Core.Fcore_FLX]
RND_FTZ.beta [in Flocq.Core.Fcore_FTZ]
RND_FTZ.prec [in Flocq.Core.Fcore_FTZ]
RND_FLX.NE_prop [in Flocq.Core.Fcore_FLX]
RND_FLX.prec [in Flocq.Core.Fcore_FLX]
RND_FTZ.emin [in Flocq.Core.Fcore_FTZ]
RND_FLT.prec [in Flocq.Core.Fcore_FLT]
RND_FTZ.FTZ_round.rnd [in Flocq.Core.Fcore_FTZ]
RND_FLT.beta [in Flocq.Core.Fcore_FLT]


Z

Zpower.r [in Flocq.Core.Fcore_Zaux]



Library Index

F

Fappli_IEEE_bits
Fappli_IEEE
Fcalc_div
Fcalc_bracket
Fcalc_round
Fcalc_ops
Fcalc_sqrt
Fcalc_digits
Fcore
Fcore_FIX
Fcore_ulp
Fcore_rnd
Fcore_Raux
Fcore_FTZ
Fcore_generic_fmt
Fcore_float_prop
Fcore_FLT
Fcore_FLX
Fcore_Zaux
Fcore_defs
Fcore_digits
Fcore_rnd_ne
Flocq_version
Fprop_Sterbenz
Fprop_div_sqrt_error
Fprop_relative
Fprop_mult_error
Fprop_plus_error



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1194 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (20 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (15 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (10 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (650 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (78 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (42 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (41 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (19 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (172 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (119 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (28 entries)

This page has been generated by coqdoc