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 (1091 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 (161 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 (33 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 (777 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 (4 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 (4 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 (1 entry)
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 (26 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 (83 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 (2 entries)

Global Index

A

absFBounded [lemma, in Float.Fbound]
absolu_lt_nz [lemma, in Float.Faux]
absolu_Zs_neg [lemma, in Float.Faux]
absolu_Zs [lemma, in Float.Faux]
absolu_comp_mult [lemma, in Float.Faux]
absolu_Zopp [lemma, in Float.Faux]
absolu_INR [lemma, in Float.Faux]
abs_lt_MSB [lemma, in Float.MSB]
AllFloat [library]
AScal2 [lemma, in Float.Closest2Prop]


B

BminusSameExp [lemma, in Float.Fprop]
BminusSameExpAux [lemma, in Float.Fprop]
BminusSameExpNeg [lemma, in Float.Fprop]
Bound [constructor, in Float.Fbound]
boundBoundNat [lemma, in Float.Fmin]
boundedNorMinGivesExp [lemma, in Float.Fnorm]
boundNat [definition, in Float.Fmin]
boundNatCorrect [lemma, in Float.Fmin]
boundNormalMult [lemma, in Float.MSBProp]
boundOnePrecision [lemma, in Float.MSBProp]
boundR [definition, in Float.Fmin]
boundRCorrect1 [lemma, in Float.Fmin]
boundRCorrect2 [lemma, in Float.Fmin]
boundRrOpp [lemma, in Float.Fmin]
bugFix [section, in Float.Paux]
bugFix.PdivAux [variable, in Float.Paux]


C

CanonicFulp [lemma, in Float.FroundProp]
Closest [definition, in Float.Closest]
Closest [library]
ClosestCompatible [lemma, in Float.Closest]
ClosestErrorBound [lemma, in Float.ClosestProp]
ClosestErrorBoundNormal [lemma, in Float.ClosestProp]
ClosestErrorBoundNormal_aux [lemma, in Float.ClosestProp]
ClosestErrorBoundNormal2_aux [lemma, in Float.ClosestProp]
ClosestErrorBound2 [lemma, in Float.ClosestProp]
ClosestErrorExp [lemma, in Float.ClosestProp]
ClosestErrorExpStrict [lemma, in Float.ClosestProp]
ClosestExp [lemma, in Float.ClosestProp]
ClosestFabs [lemma, in Float.ClosestProp]
ClosestIdem [lemma, in Float.ClosestProp]
closestLessMultAbs [lemma, in Float.ClosestMult]
closestLessMultNeg [lemma, in Float.ClosestMult]
closestLessMultPos [lemma, in Float.ClosestMult]
ClosestMax [lemma, in Float.Closest]
ClosestMaxEq [lemma, in Float.Closest]
ClosestMin [lemma, in Float.Closest]
ClosestMinEq [lemma, in Float.Closest]
ClosestMinOrMax [lemma, in Float.Closest]
ClosestMonotone [lemma, in Float.Closest]
ClosestMult [library]
ClosestM1 [lemma, in Float.ClosestProp]
ClosestOpp [lemma, in Float.ClosestProp]
ClosestP [section, in Float.ClosestPlus]
ClosestPlus [library]
ClosestProp [library]
ClosestPropHigham25 [lemma, in Float.ClosestProp]
ClosestP.b [variable, in Float.ClosestPlus]
ClosestP.FtoRradix [variable, in Float.ClosestPlus]
ClosestP.pGivesBound [variable, in Float.ClosestPlus]
ClosestP.precision [variable, in Float.ClosestPlus]
ClosestP.precisionGreaterThanOne [variable, in Float.ClosestPlus]
ClosestP.radix [variable, in Float.ClosestPlus]
ClosestP.radixMoreThanOne [variable, in Float.ClosestPlus]
ClosestP.radixMoreThanZERO [variable, in Float.ClosestPlus]
ClosestRoundedModeP [lemma, in Float.Closest]
ClosestSymmetric [lemma, in Float.Closest]
ClosestTotal [lemma, in Float.Closest]
ClosestUlp [lemma, in Float.ClosestProp]
Closest2Plus [library]
Closest2Prop [library]
compare_SUP_dec [lemma, in Float.Paux]
comparisons [section, in Float.Fcomp]
comparisons.FtoRradix [variable, in Float.Fcomp]
comparisons.radix [variable, in Float.Fcomp]
comparisons.radixMoreThanOne [variable, in Float.Fcomp]
comparisons.radixMoreThanZERO [variable, in Float.Fcomp]
CompatibleP [definition, in Float.Fround]
Contradict1 [lemma, in Float.sTactic]
Contradict2 [lemma, in Float.sTactic]
Contradict3 [lemma, in Float.sTactic]
convert_not_O [lemma, in Float.Faux]


D

definitions [section, in Float.Float]
definitions.radix [variable, in Float.Float]
definitions.radixMoreThanOne [variable, in Float.Float]
definitions.radixMoreThanZERO [variable, in Float.Float]
dExp [projection, in Float.Fbound]
digit [definition, in Float.Digit]
Digit [library]
digitAdd [lemma, in Float.Digit]
digitAux [definition, in Float.Digit]
digitAuxLess [lemma, in Float.Digit]
digitAuxMore [lemma, in Float.Digit]
digitAux1 [lemma, in Float.Digit]
digitGivesBoundedNum [lemma, in Float.Fnorm]
digitInv [lemma, in Float.Digit]
digitLess [lemma, in Float.Digit]
digitMore [lemma, in Float.Digit]
digitnNormMin [lemma, in Float.Fnorm]
digitNotZero [lemma, in Float.Digit]
digitO [lemma, in Float.Digit]
digitPredVNumiSPrecision [lemma, in Float.Fnorm]
digitVNumiSPrecision [lemma, in Float.Fnorm]
digit_anti_monotone_lt [lemma, in Float.Digit]
digit_abs [lemma, in Float.Digit]
digit_bound [lemma, in Float.Digit]
digit_minus1 [lemma, in Float.Digit]
digit_monotone [lemma, in Float.Digit]
digit1 [lemma, in Float.Digit]
div2IsBetween [lemma, in Float.FroundProp]
div2IsBetweenPos [lemma, in Float.FroundProp]


E

eqExpLess [lemma, in Float.Fbound]
eqExpMax [lemma, in Float.Fbound]
errorBoundedMult [lemma, in Float.FroundMult]
errorBoundedMultClosest [lemma, in Float.ClosestMult]
errorBoundedMultClosest_aux [lemma, in Float.ClosestMult]
errorBoundedMultExp [lemma, in Float.FroundMult]
errorBoundedMultExpPos [lemma, in Float.FroundMult]
errorBoundedMultExp_aux [lemma, in Float.FroundMult]
errorBoundedMultMax [lemma, in Float.FroundMult]
errorBoundedMultMin [lemma, in Float.FroundMult]
errorBoundedMultNeg [lemma, in Float.FroundMult]
errorBoundedMultPos [lemma, in Float.FroundMult]
errorBoundedPlus [lemma, in Float.ClosestPlus]
errorBoundedPlusAbs [lemma, in Float.ClosestPlus]
errorBoundedPlusLe [lemma, in Float.ClosestPlus]
Even [definition, in Float.Fodd]
EvenClosest [definition, in Float.Closest]
EvenClosestCompatible [lemma, in Float.Closest]
EvenClosestMinOrMax [lemma, in Float.Closest]
EvenClosestMonotone [lemma, in Float.Closest]
EvenClosestRoundedModeP [lemma, in Float.Closest]
EvenClosestSymmetric [lemma, in Float.Closest]
EvenClosestTotal [lemma, in Float.Closest]
EvenClosestUniqueP [lemma, in Float.Closest]
EvenExp [lemma, in Float.Fodd]
EvenFNSuccFNSuccMid [lemma, in Float.Closest2Prop]
EvenMultInv [lemma, in Float.Fodd]
EvenMult1 [lemma, in Float.Fodd]
EvenMult2 [lemma, in Float.Fodd]
EvenNOdd [lemma, in Float.Fodd]
EvenO [lemma, in Float.Fodd]
EvenOpp [lemma, in Float.Fodd]
EvenPlusInv1 [lemma, in Float.Fodd]
EvenPlusInv2 [lemma, in Float.Fodd]
EvenPlus1 [lemma, in Float.Fodd]
EvenPlus2 [lemma, in Float.Fodd]
EvenSOdd [lemma, in Float.Fodd]
EvenSOddInv [lemma, in Float.Fodd]
ExactMinusInterval [lemma, in Float.FroundPlus]
ExactMinusIntervalAux [lemma, in Float.FroundPlus]
ExactMinusIntervalAux1 [lemma, in Float.FroundPlus]
exp [definition, in Float.Paux]
expPlus [lemma, in Float.Paux]


F

Fabs [definition, in Float.Fop]
Fabs_Fzero [lemma, in Float.Fop]
Fabs_correct [lemma, in Float.Fop]
Fabs_correct2 [lemma, in Float.Fop]
Fabs_correct1 [lemma, in Float.Fop]
Faux [library]
Fbound [record, in Float.Fbound]
Fbound [library]
Fbounded [definition, in Float.Fbound]
FboundedEqExp [lemma, in Float.Fbound]
FboundedEqExpPos [lemma, in Float.Fbound]
FboundedExp [lemma, in Float.Fbound]
FboundedFzero [lemma, in Float.Fbound]
FboundedMbound [lemma, in Float.Fnorm]
FboundedMboundPos [lemma, in Float.Fnorm]
FboundedNum [lemma, in Float.Fbound]
FboundedOne [lemma, in Float.Fnorm]
FBoundedPred [lemma, in Float.FPred]
FBoundedScale [lemma, in Float.Fbound]
FboundedShiftLess [lemma, in Float.Fbound]
FBoundedSuc [lemma, in Float.FSucc]
FboundedZeroSameExp [lemma, in Float.Fbound]
Fbounded_Def.FtoRradix [variable, in Float.Fbound]
Fbounded_Def.radixMoreThanZERO [variable, in Float.Fbound]
Fbounded_Def.radixMoreThanOne [variable, in Float.Fbound]
Fbounded_Def.radix [variable, in Float.Fbound]
Fbounded_Def [section, in Float.Fbound]
FboundNext [lemma, in Float.Fnorm]
Fcanonic [definition, in Float.Fnorm]
FcanonicBound [lemma, in Float.Fnorm]
FcanonicFabs [lemma, in Float.Fnorm]
FcanonicFnormalizeEq [lemma, in Float.Fnorm]
FcanonicFopp [lemma, in Float.Fnorm]
FcanonicLeastExp [lemma, in Float.Fnorm]
FcanonicLePos [lemma, in Float.Fnorm]
FcanonicLtNeg [lemma, in Float.Fnorm]
FcanonicLtPos [lemma, in Float.Fnorm]
FcanonicNegFexpRlt [lemma, in Float.Fnorm]
FcanonicNnormMin [lemma, in Float.Fnorm]
FcanonicPosFexpRlt [lemma, in Float.Fnorm]
FcanonicPpred [lemma, in Float.Fnorm]
FcanonicUnique [lemma, in Float.Fnorm]
Fcanonic_Rle_Zle [lemma, in Float.Fnorm]
Fclosest [section, in Float.Closest]
Fclosestp2 [section, in Float.ClosestProp]
Fclosestp2.b [variable, in Float.ClosestProp]
Fclosestp2.FtoRradix [variable, in Float.ClosestProp]
Fclosestp2.pGivesBound [variable, in Float.ClosestProp]
Fclosestp2.precision [variable, in Float.ClosestProp]
Fclosestp2.precisionGreaterThanOne [variable, in Float.ClosestProp]
Fclosestp2.radix [variable, in Float.ClosestProp]
Fclosestp2.radixMoreThanOne [variable, in Float.ClosestProp]
Fclosestp2.radixMoreThanZERO [variable, in Float.ClosestProp]
Fclosest.b [variable, in Float.Closest]
Fclosest.FtoRradix [variable, in Float.Closest]
Fclosest.pGivesBound [variable, in Float.Closest]
Fclosest.precision [variable, in Float.Closest]
Fclosest.precisionGreaterThanOne [variable, in Float.Closest]
Fclosest.radix [variable, in Float.Closest]
Fclosest.radixMoreThanOne [variable, in Float.Closest]
Fcomp [library]
Fcompare [definition, in Float.Fcomp]
Fdiff [definition, in Float.Fcomp]
Fdiff_correct [lemma, in Float.Fcomp]
Fdigit [definition, in Float.Float]
FdigitEq [lemma, in Float.Float]
Fdigit_abs [lemma, in Float.Fop]
Fdigit_opp [lemma, in Float.Fop]
Feq [definition, in Float.Fcomp]
Feq_bool_correct_f [lemma, in Float.Fcomp]
Feq_bool_correct_r [lemma, in Float.Fcomp]
Feq_bool_correct_t [lemma, in Float.Fcomp]
Feq_bool [definition, in Float.Fcomp]
Feven [definition, in Float.Fodd]
FEvenD [lemma, in Float.Fodd]
FevenFop [lemma, in Float.Fodd]
FevenNormMin [lemma, in Float.Closest2Prop]
FevenO [lemma, in Float.Fodd]
FevenOrFodd [lemma, in Float.Fodd]
FevenPred [lemma, in Float.Fodd]
FevenSuc [lemma, in Float.Fodd]
FevenSucProp [lemma, in Float.Fodd]
Fexp [projection, in Float.Float]
Fexp_le_MSB [lemma, in Float.MSB]
Fexp_le_LSB [lemma, in Float.MSB]
Fge [definition, in Float.Fcomp]
Fge_Zge [lemma, in Float.Fcomp]
Fgt [definition, in Float.Fcomp]
Fgt_Zgt [lemma, in Float.Fcomp]
finduct [section, in Float.Finduct]
Finduct [library]
FinductNeg [lemma, in Float.Finduct]
FinductNegAux [lemma, in Float.Finduct]
FinductPos [lemma, in Float.Finduct]
FinductPosAux [lemma, in Float.Finduct]
finduct.b [variable, in Float.Finduct]
finduct.FtoRradix [variable, in Float.Finduct]
finduct.pGivesBound [variable, in Float.Finduct]
finduct.precision [variable, in Float.Finduct]
finduct.precisionNotZero [variable, in Float.Finduct]
finduct.radix [variable, in Float.Finduct]
finduct.radixMoreThanOne [variable, in Float.Finduct]
finduct.radixMoreThanZERO [variable, in Float.Finduct]
firstNormalPos [definition, in Float.Fnorm]
firstNormalPosNormal [lemma, in Float.Fnorm]
Fle [definition, in Float.Fcomp]
Fle_trans [lemma, in Float.Fcomp]
Fle_refl [lemma, in Float.Fcomp]
Fle_Fge [lemma, in Float.Fcomp]
Fle_Zle [lemma, in Float.Fcomp]
Fle_bool_correct_f [lemma, in Float.Fcomp]
Fle_bool_correct_r [lemma, in Float.Fcomp]
Fle_bool_correct_t [lemma, in Float.Fcomp]
Fle_bool [definition, in Float.Fcomp]
float [record, in Float.Float]
Float [constructor, in Float.Float]
Float [library]
floatDec [lemma, in Float.Float]
floatEq [lemma, in Float.Float]
Flt [definition, in Float.Fcomp]
Flt_Fgt [lemma, in Float.Fcomp]
Flt_Zlt [lemma, in Float.Fcomp]
Flt_bool_correct_f [lemma, in Float.Fcomp]
Flt_bool_correct_r [lemma, in Float.Fcomp]
Flt_bool_correct_t [lemma, in Float.Fcomp]
Flt_bool [definition, in Float.Fcomp]
FmaxRep [lemma, in Float.Fmin]
Fmin [library]
FMinMax [section, in Float.Fmin]
FMinMax.b [variable, in Float.Fmin]
FMinMax.FtoRradix [variable, in Float.Fmin]
FMinMax.pGivesBound [variable, in Float.Fmin]
FMinMax.precision [variable, in Float.Fmin]
FMinMax.precisionNotZero [variable, in Float.Fmin]
FMinMax.radix [variable, in Float.Fmin]
FMinMax.radixMoreThanOne [variable, in Float.Fmin]
FMinMax.radixMoreThanZERO [variable, in Float.Fmin]
FminRep [lemma, in Float.Fmin]
Fminus [definition, in Float.Fop]
Fminus_correct [lemma, in Float.Fop]
Fmult [definition, in Float.Fop]
FmultRadixInv [lemma, in Float.ClosestProp]
Fmult_correct [definition, in Float.Fop]
FNeven [definition, in Float.Fodd]
FNEvenD [lemma, in Float.Fodd]
FNevenEq [lemma, in Float.Fodd]
FNevenFop [lemma, in Float.Fodd]
FNevenOrFNodd [lemma, in Float.Fodd]
FNevenPred [lemma, in Float.Fodd]
FNevenSuc [lemma, in Float.Fodd]
FNodd [definition, in Float.Fodd]
FNoddEq [lemma, in Float.Fodd]
FNoddFop [lemma, in Float.Fodd]
FnOddNEven [lemma, in Float.Fodd]
FNoddPred [lemma, in Float.Fodd]
FNoddSuc [lemma, in Float.Fodd]
Fnorm [library]
Fnormal [definition, in Float.Fnorm]
FnormalBound [lemma, in Float.Fnorm]
FnormalBoundAbs [lemma, in Float.Fnorm]
FnormalBoundAbs2 [lemma, in Float.Fnorm]
FnormalBounded [lemma, in Float.Fnorm]
FnormalFabs [lemma, in Float.Fnorm]
FnormalFop [lemma, in Float.Fnorm]
Fnormalize [definition, in Float.Fnorm]
FnormalizeBounded [lemma, in Float.Fnorm]
FnormalizeCanonic [lemma, in Float.Fnorm]
FnormalizeCorrect [lemma, in Float.Fnorm]
Fnormalized_Def.pGivesBound [variable, in Float.Fnorm]
Fnormalized_Def.precisionNotZero [variable, in Float.Fnorm]
Fnormalized_Def.precision [variable, in Float.Fnorm]
Fnormalized_Def.b [variable, in Float.Fnorm]
Fnormalized_Def.FtoRradix [variable, in Float.Fnorm]
Fnormalized_Def.radixMoreThanZERO [variable, in Float.Fnorm]
Fnormalized_Def.radixMoreThanOne [variable, in Float.Fnorm]
Fnormalized_Def.radix [variable, in Float.Fnorm]
Fnormalized_Def [section, in Float.Fnorm]
Fnormalize_Fopp [lemma, in Float.Fnorm]
FnormalLtFirstNormalNeg [lemma, in Float.Fnorm]
FnormalLtFirstNormalPos [lemma, in Float.Fnorm]
FnormalLtNeg [lemma, in Float.Fnorm]
FnormalLtPos [lemma, in Float.Fnorm]
FnormalNnormMin [lemma, in Float.Fnorm]
FnormalNotZero [lemma, in Float.Fnorm]
FnormalPpred [lemma, in Float.Fnorm]
FnormalPrecision [lemma, in Float.Fnorm]
FnormalUnique [lemma, in Float.Fnorm]
FNPred [definition, in Float.FPred]
FNPredCanonic [lemma, in Float.FPred]
FNPredFopFNSucc [lemma, in Float.FPred]
FNPredLt [lemma, in Float.FPred]
FNPredProp [lemma, in Float.FPred]
FNPredSuc [lemma, in Float.FPred]
FNPredSucEq [lemma, in Float.FPred]
FNSucc [definition, in Float.FSucc]
FNSuccCanonic [lemma, in Float.FSucc]
FNSuccEq [lemma, in Float.FSucc]
FNSuccFNSuccMid [lemma, in Float.FSucc]
FNSuccLt [lemma, in Float.FSucc]
FNSuccProp [lemma, in Float.FSucc]
FNSuccUlpPos [lemma, in Float.FroundProp]
FNSucPred [lemma, in Float.FPred]
FNSucPredEq [lemma, in Float.FPred]
Fnum [projection, in Float.Float]
Fodd [definition, in Float.Fodd]
FOdd [section, in Float.Fodd]
Fodd [library]
FoddFop [lemma, in Float.Fodd]
FoddPred [lemma, in Float.Fodd]
FoddSuc [lemma, in Float.Fodd]
FOdd.b [variable, in Float.Fodd]
FOdd.FtoRradix [variable, in Float.Fodd]
FOdd.pGivesBound [variable, in Float.Fodd]
FOdd.precision [variable, in Float.Fodd]
FOdd.precisionGreaterThanOne [variable, in Float.Fodd]
FOdd.radix [variable, in Float.Fodd]
FOdd.radixMoreThanOne [variable, in Float.Fodd]
FOdd.radixMoreThanZERO [variable, in Float.Fodd]
Fop [library]
Fopp [definition, in Float.Fop]
Fopp_Fminus_dist [lemma, in Float.Fop]
Fopp_Fminus [lemma, in Float.Fop]
Fopp_Fopp [lemma, in Float.Fop]
Fopp_correct [lemma, in Float.Fop]
FopRepAux [lemma, in Float.Fbound]
Fplus [definition, in Float.Fop]
Fplus_correct [lemma, in Float.Fop]
FPred [definition, in Float.FPred]
FPred [library]
FPredCanonic [lemma, in Float.FPred]
FPredDiff1 [lemma, in Float.FPred]
FPredDiff2 [lemma, in Float.FPred]
FPredDiff3 [lemma, in Float.FPred]
FPredFopFSucc [lemma, in Float.FPred]
FPredLt [lemma, in Float.FPred]
FPredProp [lemma, in Float.FPred]
FPredSimpl1 [lemma, in Float.FPred]
FPredSimpl2 [lemma, in Float.FPred]
FPredSimpl3 [lemma, in Float.FPred]
FPredSimpl4 [lemma, in Float.FPred]
FPredSuc [lemma, in Float.FPred]
FpredUlpPos [lemma, in Float.ClosestProp]
FPredZleEq [lemma, in Float.FPred]
Fprop [section, in Float.Fprop]
Fprop [library]
Fprop.b [variable, in Float.Fprop]
Fprop.FtoRradix [variable, in Float.Fprop]
Fprop.radix [variable, in Float.Fprop]
Fprop.radixMoreThanOne [variable, in Float.Fprop]
FRound [section, in Float.Fround]
Fround [library]
FroundMult [library]
FRoundP [section, in Float.FroundProp]
FRoundP [section, in Float.FroundMult]
FRoundP [section, in Float.FroundPlus]
FRoundP [section, in Float.ClosestMult]
FroundPlus [library]
FroundProp [library]
FRoundP.b [variable, in Float.FroundProp]
FRoundP.b [variable, in Float.FroundMult]
FRoundP.b [variable, in Float.FroundPlus]
FRoundP.b [variable, in Float.ClosestMult]
FRoundP.FtoRradix [variable, in Float.FroundProp]
FRoundP.FtoRradix [variable, in Float.FroundMult]
FRoundP.FtoRradix [variable, in Float.FroundPlus]
FRoundP.FtoRradix [variable, in Float.ClosestMult]
FRoundP.pGivesBound [variable, in Float.FroundProp]
FRoundP.pGivesBound [variable, in Float.FroundMult]
FRoundP.pGivesBound [variable, in Float.FroundPlus]
FRoundP.pGivesBound [variable, in Float.ClosestMult]
FRoundP.precision [variable, in Float.FroundProp]
FRoundP.precision [variable, in Float.FroundMult]
FRoundP.precision [variable, in Float.FroundPlus]
FRoundP.precision [variable, in Float.ClosestMult]
FRoundP.precisionGreaterThanOne [variable, in Float.FroundProp]
FRoundP.precisionGreaterThanOne [variable, in Float.FroundMult]
FRoundP.precisionGreaterThanOne [variable, in Float.FroundPlus]
FRoundP.precisionGreaterThanOne [variable, in Float.ClosestMult]
FRoundP.radix [variable, in Float.FroundProp]
FRoundP.radix [variable, in Float.FroundMult]
FRoundP.radix [variable, in Float.FroundPlus]
FRoundP.radix [variable, in Float.ClosestMult]
FRoundP.radixMoreThanOne [variable, in Float.FroundProp]
FRoundP.radixMoreThanOne [variable, in Float.FroundMult]
FRoundP.radixMoreThanOne [variable, in Float.FroundPlus]
FRoundP.radixMoreThanOne [variable, in Float.ClosestMult]
FRoundP.radixMoreThanZERO [variable, in Float.FroundProp]
FRoundP.radixMoreThanZERO [variable, in Float.FroundMult]
FRoundP.radixMoreThanZERO [variable, in Float.FroundPlus]
FRound.b [variable, in Float.Fround]
FRound.FtoRradix [variable, in Float.Fround]
FRound.pGivesBound [variable, in Float.Fround]
FRound.precision [variable, in Float.Fround]
FRound.precisionGreaterThanOne [variable, in Float.Fround]
FRound.radix [variable, in Float.Fround]
FRound.radixMoreThanOne [variable, in Float.Fround]
Fshift [definition, in Float.Float]
FshiftAdd [lemma, in Float.Float]
FshiftCorrect [lemma, in Float.Float]
FshiftCorrectInv [lemma, in Float.Float]
FshiftCorrectSym [lemma, in Float.Float]
FshiftFdigit [lemma, in Float.Float]
FshiftO [lemma, in Float.Float]
Fsubnormal [definition, in Float.Fnorm]
FsubnormalBound [lemma, in Float.Fnorm]
FsubnormalDigit [lemma, in Float.Fnorm]
FsubnormalFbounded [lemma, in Float.Fnorm]
FsubnormalFexp [lemma, in Float.Fnorm]
FsubnormalLt [lemma, in Float.Fnorm]
FsubnormalLtFirstNormalPos [lemma, in Float.Fnorm]
FsubnormalnormalLtNeg [lemma, in Float.Fnorm]
FsubnormalnormalLtPos [lemma, in Float.Fnorm]
FsubnormalUnique [lemma, in Float.Fnorm]
FsubnormFabs [lemma, in Float.Fnorm]
FsubnormFopp [lemma, in Float.Fnorm]
FSucc [definition, in Float.FSucc]
FSucc [library]
FSuccCanonic [lemma, in Float.FSucc]
FSuccDiffPos [lemma, in Float.FroundProp]
FSuccDiff1 [lemma, in Float.FSucc]
FSuccDiff2 [lemma, in Float.FSucc]
FSuccDiff3 [lemma, in Float.FSucc]
FSuccLt [lemma, in Float.FSucc]
FSuccNegCanonic [lemma, in Float.FSucc]
FSuccNormNegNormMin [lemma, in Float.FSucc]
FSuccNormNegNotNormMin [lemma, in Float.FSucc]
FSuccNormPos [lemma, in Float.FSucc]
FSuccPosNotMax [lemma, in Float.FSucc]
FSuccProp [lemma, in Float.FSucc]
FSuccPropNeg [lemma, in Float.FSucc]
FSuccPropPos [lemma, in Float.FSucc]
FSuccSimpl1 [lemma, in Float.FSucc]
FSuccSimpl2 [lemma, in Float.FSucc]
FSuccSimpl3 [lemma, in Float.FSucc]
FSuccSimpl4 [lemma, in Float.FSucc]
FSuccSubnormal [lemma, in Float.FSucc]
FSuccSubnormNearNormMin [lemma, in Float.FSucc]
FSuccSubnormNotNearNormMin [lemma, in Float.FSucc]
FSuccUlpPos [lemma, in Float.FroundProp]
FSuccZleEq [lemma, in Float.FSucc]
FSucFSucMid [lemma, in Float.FSucc]
FSucPred [lemma, in Float.FPred]
FtoR [definition, in Float.Float]
FtoREqInv1 [lemma, in Float.Float]
FtoREqInv2 [lemma, in Float.Float]
Fulp [definition, in Float.FroundProp]
FulpComp [lemma, in Float.FroundProp]
FulpFabs [lemma, in Float.FroundProp]
FulpFPredGePos [lemma, in Float.FroundProp]
FulpFPredLe [lemma, in Float.ClosestProp]
FulpGe [lemma, in Float.FroundProp]
FulpLe [lemma, in Float.FroundProp]
FulpLe2 [lemma, in Float.FroundProp]
FulpPred [lemma, in Float.FroundProp]
FulpPredCan [lemma, in Float.FroundProp]
FulpSuc [lemma, in Float.FroundProp]
FulpSucCan [lemma, in Float.FroundProp]
FUlp_Le_LSigB [lemma, in Float.FroundProp]
Fulp_zero [lemma, in Float.FroundProp]
FvalScale [lemma, in Float.Fbound]
Fweight [definition, in Float.Finduct]
FweightEq [lemma, in Float.Finduct]
FweightLt [lemma, in Float.Finduct]
FweightZle [lemma, in Float.Finduct]
Fzero [definition, in Float.Float]
FzeroisReallyZero [lemma, in Float.Float]
FzeroisZero [lemma, in Float.Fbound]
Fzero_opp [lemma, in Float.Fop]
F2 [section, in Float.Closest2Plus]
F2 [section, in Float.Closest2Prop]
F2.b [variable, in Float.Closest2Plus]
F2.b [variable, in Float.Closest2Prop]
F2.FtoRradix [variable, in Float.Closest2Plus]
F2.FtoRradix [variable, in Float.Closest2Prop]
F2.pGivesBound [variable, in Float.Closest2Plus]
F2.pGivesBound [variable, in Float.Closest2Prop]
F2.precision [variable, in Float.Closest2Plus]
F2.precision [variable, in Float.Closest2Prop]
F2.precisionNotZero [variable, in Float.Closest2Plus]
F2.precisionNotZero [variable, in Float.Closest2Prop]
F2.radix [variable, in Float.Closest2Plus]
F2.radix [variable, in Float.Closest2Prop]


I

InBinade [lemma, in Float.FroundProp]
inject_nat_eq [lemma, in Float.Faux]
inject_nat_convert [lemma, in Float.Faux]
inj_pred [lemma, in Float.Faux]
inj_abs [lemma, in Float.Faux]
inj_oZ1 [lemma, in Float.Zdivides]
INR_inv [lemma, in Float.Faux]
INR_lt_nm [lemma, in Float.Faux]
Int_part_IZR [lemma, in Float.Faux]
Int_part_INR [lemma, in Float.Faux]
in_map_inv [lemma, in Float.Zenum]
isBounded [lemma, in Float.Fbound]
isMax [definition, in Float.Fmin]
isMaxComp [lemma, in Float.FroundProp]
isMax_inv1 [lemma, in Float.Fmin]
isMin [definition, in Float.Fmin]
isMinComp [lemma, in Float.FroundProp]
isMin_inv1 [lemma, in Float.Fmin]
is_Fzero_rep2 [lemma, in Float.Float]
is_Fzero_rep1 [lemma, in Float.Float]
is_FzeroP [lemma, in Float.Float]
is_Fzero [definition, in Float.Float]
IZR_inv [lemma, in Float.Faux]
IZR_zero_r [lemma, in Float.Faux]
IZR_zero [lemma, in Float.Faux]


L

LeFnumZERO [lemma, in Float.Fcomp]
LeFulpPos [lemma, in Float.FroundProp]
LeR0Fnum [lemma, in Float.Fcomp]
LessExpBound [lemma, in Float.Fbound]
LeZEROFnum [lemma, in Float.Fcomp]
le_Rle [lemma, in Float.Faux]
le_mult_anti_compatibility [lemma, in Float.Faux]
le_next [lemma, in Float.Faux]
le_refl_eq [lemma, in Float.Faux]
LSB [definition, in Float.MSB]
LSBMinus [lemma, in Float.FroundPlus]
LSBPlus [lemma, in Float.FroundPlus]
LSB_rep_min [lemma, in Float.MSB]
LSB_rep [lemma, in Float.MSB]
LSB_le_abs [lemma, in Float.MSB]
LSB_le_MSB [lemma, in Float.MSB]
LSB_abs [lemma, in Float.MSB]
LSB_opp [lemma, in Float.MSB]
LSB_comp [lemma, in Float.MSB]
LSB_shift [lemma, in Float.MSB]
lte_comp_mult [lemma, in Float.Faux]
LtFnumZERO [lemma, in Float.Float]
LtFsubnormal [lemma, in Float.Fnorm]
LtR0Fnum [lemma, in Float.Fcomp]
lt_S_le [lemma, in Float.Faux]
lt_Zlt_inv [lemma, in Float.Faux]
lt_Rlt [lemma, in Float.Faux]
lt_mult_anti_compatibility [lemma, in Float.Faux]
lt_minus_inv [lemma, in Float.Faux]
lt_next [lemma, in Float.Faux]
lt_comp_mult [lemma, in Float.Faux]
lt_comp_mult_r [lemma, in Float.Faux]
lt_comp_mult_l [lemma, in Float.Faux]
lt_le_pred [lemma, in Float.Faux]


M

MaxBinade [lemma, in Float.Fmin]
MaxCompatible [lemma, in Float.Fround]
maxDiv [definition, in Float.MSB]
maxDivCorrect [lemma, in Float.MSB]
maxDivLess [lemma, in Float.MSB]
maxDivLt [lemma, in Float.MSB]
maxDivPlus [lemma, in Float.MSB]
maxDivSimpl [lemma, in Float.MSB]
maxDivSimplAux [lemma, in Float.MSB]
maxDivSimplInv [lemma, in Float.MSB]
maxDivSimplInvAux [lemma, in Float.MSB]
maxDivUnique [lemma, in Float.MSB]
maxDivUniqueDigit [lemma, in Float.MSB]
maxDivUniqueInverse [lemma, in Float.MSB]
maxDivUniqueInverseDigit [lemma, in Float.MSB]
maxDiv_abs [lemma, in Float.MSB]
maxDiv_opp [lemma, in Float.MSB]
MaxEq [lemma, in Float.Fmin]
MaxEx [lemma, in Float.Fmin]
maxFbounded [lemma, in Float.Fbound]
MaxFloat [lemma, in Float.Fnorm]
maxMax [lemma, in Float.Fbound]
maxMaxBis [lemma, in Float.Fnorm]
maxMax1 [lemma, in Float.Fnorm]
MaxMin [lemma, in Float.Fmin]
MaxOppMin [lemma, in Float.Fmin]
MaxRoundedModeP [lemma, in Float.Fround]
MaxUniqueP [lemma, in Float.Fround]
mBFadic_correct4 [lemma, in Float.Fmin]
mBFadic_correct3 [lemma, in Float.Fmin]
mBFadic_correct2 [lemma, in Float.Fmin]
mBFadic_correct1 [lemma, in Float.Fmin]
mBFloat [definition, in Float.Fmin]
mBPadic_Fbounded [lemma, in Float.Fmin]
mf [section, in Float.MSB]
mf.FtoRradix [variable, in Float.MSB]
mf.radix [variable, in Float.MSB]
mf.radixMoreThanOne [variable, in Float.MSB]
mf.radixMoreThanZERO [variable, in Float.MSB]
MinBinade [lemma, in Float.Fmin]
MinCompatible [lemma, in Float.Fround]
MinEq [lemma, in Float.Fmin]
MinEx [lemma, in Float.Fmin]
MinExList [lemma, in Float.Fmin]
MinMax [lemma, in Float.Fmin]
MinOppMax [lemma, in Float.Fmin]
MinOrMaxP [definition, in Float.Fround]
MinOrMaxRep [lemma, in Float.Fround]
MinRoundedModeP [lemma, in Float.Fround]
MinUniqueP [lemma, in Float.Fround]
minusRoundRep [lemma, in Float.FroundPlus]
minusSameExp [lemma, in Float.Fop]
minus_le [lemma, in Float.Faux]
minus_inv_lt [lemma, in Float.Faux]
minus_inv_lt_aux [lemma, in Float.Faux]
minus_minus [lemma, in Float.Faux]
min_n_0 [lemma, in Float.Faux]
min_or [lemma, in Float.Faux]
MonotoneMax [lemma, in Float.Fmin]
MonotoneMin [lemma, in Float.Fmin]
MonotoneP [definition, in Float.Fmin]
mProd [definition, in Float.Zenum]
mProd_correct_rev2 [lemma, in Float.Zenum]
mProd_correct_rev1 [lemma, in Float.Zenum]
mProd_correct [lemma, in Float.Zenum]
MSB [definition, in Float.MSB]
MSB [library]
MSBBoundNotZero [lemma, in Float.FroundProp]
MSBisMin [lemma, in Float.FroundProp]
MSBProp [section, in Float.MSBProp]
MSBProp [library]
MSBProp.b [variable, in Float.MSBProp]
MSBProp.FtoRradix [variable, in Float.MSBProp]
MSBProp.pGivesBound [variable, in Float.MSBProp]
MSBProp.precision [variable, in Float.MSBProp]
MSBProp.precisionGreaterThanOne [variable, in Float.MSBProp]
MSBProp.radix [variable, in Float.MSBProp]
MSBProp.radixMoreThanOne [variable, in Float.MSBProp]
MSBProp.radixMoreThanZERO [variable, in Float.MSBProp]
MSBroundLSB [lemma, in Float.FroundPlus]
MSBtoZero [lemma, in Float.FroundProp]
MSB_mix [lemma, in Float.MSB]
MSB_le_mult [lemma, in Float.MSB]
MSB_le_multAux [lemma, in Float.MSB]
MSB_monotone [lemma, in Float.MSB]
MSB_monotoneAux [lemma, in Float.MSB]
MSB_le_abs [lemma, in Float.MSB]
MSB_abs [lemma, in Float.MSB]
MSB_opp [lemma, in Float.MSB]
MSB_comp [lemma, in Float.MSB]
MSB_shift [lemma, in Float.MSB]
multExpMin [lemma, in Float.FroundMult]
multExpUpperBound [lemma, in Float.FroundMult]
mult_eq_inv [lemma, in Float.Faux]
mult_le_MSB [lemma, in Float.MSB]
mult_le_MSBAux [lemma, in Float.MSB]
mZlist [definition, in Float.Zenum]
mZlist_correct_rev2 [lemma, in Float.Zenum]
mZlist_correct_rev1 [lemma, in Float.Zenum]
mZlist_correct [lemma, in Float.Zenum]
mZlist_aux_correct_rev2 [lemma, in Float.Zenum]
mZlist_aux_correct_rev1 [lemma, in Float.Zenum]
mZlist_aux_correct [lemma, in Float.Zenum]
mZlist_aux [definition, in Float.Zenum]


N

natEq [definition, in Float.Faux]
NconvertO [lemma, in Float.Faux]
NDivides_minus [lemma, in Float.Zdivides]
NEq_IZRO [lemma, in Float.Faux]
NEq_INR1 [lemma, in Float.Faux]
NEq_INRO [lemma, in Float.Faux]
NEq_INR [lemma, in Float.Faux]
NisFzeroComp [lemma, in Float.Float]
nNormMimLtvNum [lemma, in Float.FSucc]
nNormMin [definition, in Float.Fnorm]
nNormPos [lemma, in Float.Fnorm]
nNrMMimLevNum [lemma, in Float.Fnorm]
None [constructor, in Float.Option]
NormalAndSubNormalNotEq [lemma, in Float.Fnorm]
NormalNotSubNormal [lemma, in Float.Fnorm]
NotDividesDigit [lemma, in Float.Zdivides]
notEqLt [lemma, in Float.Faux]
NotZmultZero [lemma, in Float.Faux]
not_O_lt [lemma, in Float.Faux]
NroundN [lemma, in Float.FroundProp]


O

Odd [definition, in Float.Fodd]
OddEvenDec [lemma, in Float.Fodd]
OddExp [lemma, in Float.Fodd]
OddMult [lemma, in Float.Fodd]
OddMultInv [lemma, in Float.Fodd]
OddNEven [lemma, in Float.Fodd]
OddOpp [lemma, in Float.Fodd]
OddPlusInv1 [lemma, in Float.Fodd]
OddPlusInv2 [lemma, in Float.Fodd]
OddPlus1 [lemma, in Float.Fodd]
OddPlus2 [lemma, in Float.Fodd]
OddSEven [lemma, in Float.Fodd]
OddSEvenInv [lemma, in Float.Fodd]
odd_even_lem [lemma, in Float.Paux]
Odd1 [lemma, in Float.Fodd]
oneExp_Zle [lemma, in Float.Float]
oneExp_Zlt [lemma, in Float.Float]
oneExp_lt [lemma, in Float.Float]
oneExp_le [lemma, in Float.Float]
oneZplus [lemma, in Float.Fop]
operations [section, in Float.Fop]
operations.FtoRradix [variable, in Float.Fop]
operations.radix [variable, in Float.Fop]
operations.radixNotZero [variable, in Float.Fop]
oppBounded [lemma, in Float.Fbound]
oppBoundedInv [lemma, in Float.Fbound]
Option [inductive, in Float.Option]
Option [library]
oZ [definition, in Float.Paux]
oZ1 [definition, in Float.Zdivides]


P

Paux [library]
Pdigit [section, in Float.Digit]
Pdigit.n [variable, in Float.Digit]
Pdigit.nMoreThanOne [variable, in Float.Digit]
Pdigit.nMoreThan1 [variable, in Float.Digit]
Pdiv [definition, in Float.Paux]
PdivBound [definition, in Float.Paux]
PdivBound_correct4 [lemma, in Float.Paux]
PdivBound_correct3 [lemma, in Float.Paux]
PdivBound_correct2 [lemma, in Float.Paux]
PdivBound_correct1 [lemma, in Float.Paux]
PdivBound_correct [lemma, in Float.Paux]
Pdivless [definition, in Float.Paux]
PdivlessAux [definition, in Float.Paux]
Pdivless_correct [lemma, in Float.Paux]
Pdivless1 [lemma, in Float.Paux]
Pdivless2 [lemma, in Float.Paux]
Pdiv_correct [lemma, in Float.Paux]
pGivesDigit [lemma, in Float.Fnorm]
plusClosestLowerBound [lemma, in Float.Closest2Plus]
plusClosestLowerBoundAux1 [lemma, in Float.Closest2Plus]
plusClosestLowerBoundAux2 [lemma, in Float.Closest2Plus]
plusErrorBound1 [lemma, in Float.ClosestPlus]
plusErrorBound1bis [lemma, in Float.ClosestPlus]
plusErrorBound1withZero [lemma, in Float.ClosestPlus]
plusErrorBound2 [lemma, in Float.Closest2Plus]
plusExactExp [lemma, in Float.ClosestPlus]
plusExactExpCanonic [lemma, in Float.ClosestPlus]
plusExactR0 [lemma, in Float.ClosestPlus]
plusExact1 [lemma, in Float.ClosestPlus]
plusExact1bis [lemma, in Float.ClosestPlus]
plusExact2 [lemma, in Float.ClosestPlus]
plusExact2Aux [lemma, in Float.ClosestPlus]
plusExpBound [lemma, in Float.FroundPlus]
plusExpMin [lemma, in Float.FroundPlus]
plusExpUpperBound [lemma, in Float.FroundPlus]
plusUpperBound [lemma, in Float.Closest2Plus]
PminPos [lemma, in Float.FroundProp]
pNormal_absolu_min [lemma, in Float.Fnorm]
positive_exp_correct [lemma, in Float.Paux]
positive_exp [definition, in Float.Paux]
PosNormMin [lemma, in Float.Fnorm]
pos_eq_bool_correct [lemma, in Float.Faux]
pos_eq_bool [definition, in Float.Faux]
pos_length_pow [lemma, in Float.Digit]
pos_length [definition, in Float.Digit]
Power [library]
powerRZ [definition, in Float.Power]
powerRZ_R1 [lemma, in Float.Power]
powerRZ_le [lemma, in Float.Power]
powerRZ_lt [lemma, in Float.Power]
powerRZ_Zs [lemma, in Float.Power]
powerRZ_Zopp [lemma, in Float.Power]
powerRZ_add [lemma, in Float.Power]
powerRZ_NOR [lemma, in Float.Power]
powerRZ_1 [lemma, in Float.Power]
powerRZ_O [lemma, in Float.Power]
powerRZ_R1 [lemma, in Float.Rpow]
powerRZ_le [lemma, in Float.Rpow]
powerRZ_lt [lemma, in Float.Rpow]
powerRZ_Zs [lemma, in Float.Rpow]
powerRZ_Zopp [lemma, in Float.Rpow]
powerRZ_add [lemma, in Float.Rpow]
powerRZ_NOR [lemma, in Float.Rpow]
powerRZ_1 [lemma, in Float.Rpow]
powerRZ_O [lemma, in Float.Rpow]
pow_R1 [lemma, in Float.Power]
pow_lt [lemma, in Float.Power]
pow_RN_plus [lemma, in Float.Power]
pow_add [lemma, in Float.Power]
pow_NR0 [lemma, in Float.Power]
pow_1 [lemma, in Float.Power]
pow_O [lemma, in Float.Power]
pow_R1 [lemma, in Float.Rpow]
pow_lt [lemma, in Float.Rpow]
pow_RN_plus [lemma, in Float.Rpow]
pow_add [lemma, in Float.Rpow]
pow_NR0 [lemma, in Float.Rpow]
pow_1 [lemma, in Float.Rpow]
pow_O [lemma, in Float.Rpow]
pPred [definition, in Float.Fnorm]
pPredMoreThanOne [lemma, in Float.ClosestPlus]
pPredMoreThanRadix [lemma, in Float.ClosestPlus]
pred [section, in Float.FPred]
pred.b [variable, in Float.FPred]
pred.FtoRradix [variable, in Float.FPred]
pred.pGivesBound [variable, in Float.FPred]
pred.precision [variable, in Float.FPred]
pred.precisionNotZero [variable, in Float.FPred]
pred.radix [variable, in Float.FPred]
pred.radixMoreThanOne [variable, in Float.FPred]
ProjectMax [lemma, in Float.Fmin]
ProjectMin [lemma, in Float.Fmin]
ProjectorP [definition, in Float.Fmin]
pSubnormal_absolu_min [lemma, in Float.Fnorm]
ptonat_def1 [lemma, in Float.Faux]
pUCanonic_absolu [lemma, in Float.Fnorm]


R

Rabsolu_Zabs [lemma, in Float.Faux]
Rabsolu_left1 [lemma, in Float.Faux]
radixRangeBoundExp [lemma, in Float.Finduct]
radixRangeBoundExp [lemma, in Float.FroundPlus]
ReqGivesEqwithSameExp [lemma, in Float.Float]
Rinv_powerRZ [lemma, in Float.Rpow]
RleBoundRoundl [lemma, in Float.FroundProp]
RleBoundRoundr [lemma, in Float.FroundProp]
Rledouble [lemma, in Float.Faux]
RleFexpFabs [lemma, in Float.Fop]
RleMaxR0 [lemma, in Float.FroundProp]
RleMinR0 [lemma, in Float.FroundProp]
RleRoundedLessR0 [lemma, in Float.FroundProp]
RleRoundedR0 [lemma, in Float.FroundProp]
Rle_Rinv [lemma, in Float.Faux]
Rle_INR [lemma, in Float.Faux]
Rle_IZR1 [lemma, in Float.Faux]
Rle_IZRO [lemma, in Float.Faux]
Rle_IZR [lemma, in Float.Faux]
Rle_R0_Ropp [lemma, in Float.Faux]
Rle_powerRZ [lemma, in Float.Power]
Rle_Float_Zle [lemma, in Float.Float]
Rle_monotony_contra_exp [lemma, in Float.Float]
Rle_monotone_exp [lemma, in Float.Float]
Rle_powerRZ [lemma, in Float.Rpow]
Rle_Fexp_eq_Zle [lemma, in Float.Fcomp]
RlIt2 [lemma, in Float.Faux]
Rltdouble [lemma, in Float.Faux]
Rlt_RinvDouble [lemma, in Float.Faux]
Rlt_IZR1 [lemma, in Float.Faux]
Rlt_IZRO [lemma, in Float.Faux]
Rlt_IZR [lemma, in Float.Faux]
Rlt_INR1 [lemma, in Float.Faux]
Rlt_R0_Ropp [lemma, in Float.Faux]
Rlt_Rminus_ZERO [lemma, in Float.Faux]
Rlt_powerRZ [lemma, in Float.Power]
Rlt_pow [lemma, in Float.Power]
Rlt_pow_R1 [lemma, in Float.Power]
Rlt_Float_Zlt [lemma, in Float.Float]
Rlt_monotony_contra_exp [lemma, in Float.Float]
Rlt_monotony_exp [lemma, in Float.Float]
Rlt_powerRZ [lemma, in Float.Rpow]
Rlt_pow [lemma, in Float.Rpow]
Rlt_pow_R1 [lemma, in Float.Rpow]
Rlt_Fexp_eq_Zlt [lemma, in Float.Fcomp]
Rlt2 [lemma, in Float.Faux]
RmaxAbs [lemma, in Float.Faux]
RmaxLess1 [lemma, in Float.Faux]
RmaxLess2 [lemma, in Float.Faux]
RmaxRmult [lemma, in Float.Faux]
RmaxSym [lemma, in Float.Faux]
Rmult_IZR [lemma, in Float.Faux]
RoundAbsMonotonel [lemma, in Float.FroundProp]
RoundAbsMonotoner [lemma, in Float.FroundProp]
RoundBound [lemma, in Float.ClosestPlus]
roundedModeAbsMult [lemma, in Float.FroundProp]
RoundedModeBounded [lemma, in Float.FroundProp]
RoundedModeErrorExpStrict [lemma, in Float.FroundProp]
roundedModeLessMult [lemma, in Float.FroundProp]
roundedModeMoreMult [lemma, in Float.FroundProp]
RoundedModeMult [lemma, in Float.FroundProp]
RoundedModeMultAbs [lemma, in Float.FroundProp]
RoundedModeMultLess [lemma, in Float.FroundProp]
RoundedModeP [definition, in Float.Fround]
RoundedModeProjectorIdem [lemma, in Float.FroundProp]
RoundedModeProjectorIdemEq [lemma, in Float.FroundProp]
RoundedModeP_inv4 [lemma, in Float.Fround]
RoundedModeP_inv3 [lemma, in Float.Fround]
RoundedModeP_inv2 [lemma, in Float.Fround]
RoundedModeP_inv1 [lemma, in Float.Fround]
RoundedModeRep [lemma, in Float.Fround]
RoundedModeUlp [lemma, in Float.FroundProp]
RoundedProjector [lemma, in Float.Fround]
RoundLessThanIsMax [lemma, in Float.Fround]
RoundLSBMax [lemma, in Float.FroundProp]
RoundMSBmax [lemma, in Float.FroundProp]
RoundMSBmin [lemma, in Float.FroundProp]
Rpow [library]
Rpow_eq_inv [lemma, in Float.Power]
Rpow_R1 [lemma, in Float.Power]
Rpow_eq_inv [lemma, in Float.Rpow]
Rpow_R1 [lemma, in Float.Rpow]
R0LeFnum [lemma, in Float.Fcomp]
R0LtFnum [lemma, in Float.Fcomp]
R0RltRlePred [lemma, in Float.FPred]
R0RltRleSucc [lemma, in Float.FSucc]


S

sameExpEq [lemma, in Float.Float]
ScalableRoundedModeP [lemma, in Float.Fround]
Some [constructor, in Float.Option]
sTactic [library]
Sterbenz [lemma, in Float.Fprop]
SterbenzAux [lemma, in Float.Fprop]
suc [section, in Float.FSucc]
suc.b [variable, in Float.FSucc]
suc.FtoRradix [variable, in Float.FSucc]
suc.pGivesBound [variable, in Float.FSucc]
suc.precision [variable, in Float.FSucc]
suc.precisionNotZero [variable, in Float.FSucc]
suc.radix [variable, in Float.FSucc]
suc.radixMoreThanOne [variable, in Float.FSucc]
suc.radixMoreThanZERO [variable, in Float.FSucc]
suc1 [section, in Float.FSucc]
suc1.b [variable, in Float.FSucc]
suc1.FtoRradix [variable, in Float.FSucc]
suc1.pGivesBound [variable, in Float.FSucc]
suc1.precision [variable, in Float.FSucc]
suc1.precisionNotZero [variable, in Float.FSucc]
suc1.radix [variable, in Float.FSucc]
suc1.radixMoreThanOne [variable, in Float.FSucc]
SymmetricP [definition, in Float.Fround]


T

ToInfinityCompatible [lemma, in Float.Fround]
ToInfinityMinOrMax [lemma, in Float.Fround]
ToInfinityMonotone [lemma, in Float.Fround]
ToInfinityP [definition, in Float.Fround]
ToInfinityRoundedModeP [lemma, in Float.Fround]
ToInfinitySymmetric [lemma, in Float.Fround]
ToInfinityTotal [lemma, in Float.Fround]
ToInfinityUniqueP [lemma, in Float.Fround]
TotalP [definition, in Float.Fround]
ToZeroCompatible [lemma, in Float.Fround]
ToZeroMinOrMax [lemma, in Float.Fround]
ToZeroMonotone [lemma, in Float.Fround]
ToZeroP [definition, in Float.Fround]
ToZeroRoundedModeP [lemma, in Float.Fround]
ToZeroSymmetric [lemma, in Float.Fround]
ToZeroTotal [lemma, in Float.Fround]
ToZeroUniqueP [lemma, in Float.Fround]
TwoMoreThanOne [lemma, in Float.Closest2Plus]
TwoMoreThanOne [lemma, in Float.Closest2Prop]


U

Ulp_Le_LSigB [lemma, in Float.MSB]
UniqueP [definition, in Float.Fround]


V

vNum [projection, in Float.Fbound]
vNumbMoreThanOne [lemma, in Float.Fnorm]
vNumPrecision [lemma, in Float.Fnorm]


Z

Zabs_intro [lemma, in Float.Faux]
Zabs_Zopp [lemma, in Float.Faux]
Zabs_Zs [lemma, in Float.Faux]
Zabs_eq_opp [lemma, in Float.Faux]
Zabs_Zmult [lemma, in Float.Faux]
Zabs_absolu [lemma, in Float.Faux]
Zabs_tri [lemma, in Float.Zdivides]
Zabs_eq_case [lemma, in Float.Zdivides]
Zcompare_EGAL [lemma, in Float.Faux]
Zcompare_correct [lemma, in Float.Digit]
Zdivides [definition, in Float.Zdivides]
Zdivides [library]
ZdividesDiv [lemma, in Float.Zdivides]
ZDividesLe [lemma, in Float.Zdivides]
ZdividesLessPow [lemma, in Float.Zdivides]
ZdividesMult [lemma, in Float.Zdivides]
ZdividesP [definition, in Float.Zdivides]
ZdividesTrans [lemma, in Float.Zdivides]
ZdividesZquotient [lemma, in Float.Zdivides]
ZdividesZquotientInv [lemma, in Float.Zdivides]
ZDivides_mult [lemma, in Float.Zdivides]
ZDivides_add [lemma, in Float.Zdivides]
Zdivides1 [lemma, in Float.Zdivides]
Zenum [library]
Zeq_Zs [lemma, in Float.Faux]
Zeq_mult_simpl [lemma, in Float.Zdivides]
Zero_le_oZ [lemma, in Float.Zdivides]
ZleAbs [lemma, in Float.Faux]
ZleLe [lemma, in Float.Faux]
Zle_Zpred_inv [lemma, in Float.Faux]
Zle_Zpred_Zlt [lemma, in Float.Faux]
Zle_n_Zpred [lemma, in Float.Faux]
Zle_Zabs_inv2 [lemma, in Float.Faux]
Zle_Zabs_inv1 [lemma, in Float.Faux]
Zle_ZERO_Zabs [lemma, in Float.Faux]
Zle_Zpred_Zpred [lemma, in Float.Faux]
Zle_Zminus_ZERO [lemma, in Float.Faux]
Zle_Zabs [lemma, in Float.Faux]
Zle_Zpred [lemma, in Float.Faux]
Zle_Rle [lemma, in Float.Faux]
Zle_abs [lemma, in Float.Faux]
Zle_Zopp_Inv [lemma, in Float.Faux]
Zle_next [lemma, in Float.Faux]
Zle_Zmult_comp_l [lemma, in Float.Faux]
Zle_Zmult_comp_r [lemma, in Float.Faux]
Zle_mult_gen [lemma, in Float.Faux]
Zle_Zopp [lemma, in Float.Faux]
Zle_monotony_contra_abs_pow [lemma, in Float.Fbound]
Zle_powerRZ [lemma, in Float.Rpow]
ZltNormMinVnum [lemma, in Float.FSucc]
Zlt_Zabs_intro [lemma, in Float.Faux]
Zlt_ZERO_Zle_ONE [lemma, in Float.Faux]
Zlt_not_eq_rev [lemma, in Float.Faux]
Zlt_not_eq [lemma, in Float.Faux]
Zlt_1_O [lemma, in Float.Faux]
Zlt_Zabs_Zpred [lemma, in Float.Faux]
Zlt_Zabs_inv2 [lemma, in Float.Faux]
Zlt_Zabs_inv1 [lemma, in Float.Faux]
Zlt_Zminus_ZERO [lemma, in Float.Faux]
Zlt_mult_ZERO [lemma, in Float.Faux]
Zlt_mult_simpl_l [lemma, in Float.Faux]
Zlt_Rlt [lemma, in Float.Faux]
Zlt_absolu [lemma, in Float.Faux]
Zlt_Zopp_Inv [lemma, in Float.Faux]
Zlt_next [lemma, in Float.Faux]
Zlt_Zopp [lemma, in Float.Faux]
Zlt_powerRZ [lemma, in Float.Power]
Zlt_powerRZ [lemma, in Float.Rpow]
Zmax [definition, in Float.Faux]
ZmaxLe1 [lemma, in Float.Faux]
ZmaxLe2 [lemma, in Float.Faux]
ZmaxSym [lemma, in Float.Faux]
Zmax_le1 [lemma, in Float.Faux]
Zmax_le2 [lemma, in Float.Faux]
Zminus_n_predm [lemma, in Float.Faux]
Zmin_Zmax [lemma, in Float.Faux]
Zmin_Zle [lemma, in Float.Faux]
Zmin_le2 [lemma, in Float.Faux]
Zmin_le1 [lemma, in Float.Faux]
Zmin_sym [lemma, in Float.Faux]
Zopp_Zpred_Zs [lemma, in Float.Faux]
Zpower_nat_1 [lemma, in Float.Faux]
Zpower_nat_O [lemma, in Float.Faux]
Zpower_nat_powerRZ_absolu [lemma, in Float.Power]
Zpower_nat_powerRZ [lemma, in Float.Power]
Zpower_NR1 [lemma, in Float.Power]
Zpower_NR0 [lemma, in Float.Power]
Zpower_nat_powerRZ_absolu [lemma, in Float.Rpow]
Zpower_nat_Z_powerRZ [lemma, in Float.Rpow]
Zpower_NR1 [lemma, in Float.Rpow]
Zpower_NR0 [lemma, in Float.Rpow]
Zpower_nat_anti_eq [lemma, in Float.Digit]
Zpower_nat_anti_monotone_le [lemma, in Float.Digit]
Zpower_nat_monotone_le [lemma, in Float.Digit]
Zpower_nat_anti_monotone_lt [lemma, in Float.Digit]
Zpower_nat_monotone_lt [lemma, in Float.Digit]
Zpower_nat_monotone_S [lemma, in Float.Digit]
Zpower_nat_less [lemma, in Float.Digit]
Zpred_Zle_Zabs_intro [lemma, in Float.Faux]
Zpred_Zopp_Zs [lemma, in Float.Faux]
Zquotient [definition, in Float.Zdivides]
ZquotientMonotone [lemma, in Float.Zdivides]
ZquotientPos [lemma, in Float.Zdivides]
ZquotientProp [lemma, in Float.Zdivides]
ZquotientUnique [lemma, in Float.Zdivides]
ZquotientZopp [lemma, in Float.Zdivides]
Zquotient_mult_comp [lemma, in Float.Zdivides]
Zquotient1 [lemma, in Float.Zdivides]
ZroundZ [lemma, in Float.FroundProp]
Z_eq_bool_correct [lemma, in Float.Faux]
Z_eq_bool [definition, in Float.Faux]
Z_O_1 [lemma, in Float.Faux]



Variable Index

B

bugFix.PdivAux [in Float.Paux]


C

ClosestP.b [in Float.ClosestPlus]
ClosestP.FtoRradix [in Float.ClosestPlus]
ClosestP.pGivesBound [in Float.ClosestPlus]
ClosestP.precision [in Float.ClosestPlus]
ClosestP.precisionGreaterThanOne [in Float.ClosestPlus]
ClosestP.radix [in Float.ClosestPlus]
ClosestP.radixMoreThanOne [in Float.ClosestPlus]
ClosestP.radixMoreThanZERO [in Float.ClosestPlus]
comparisons.FtoRradix [in Float.Fcomp]
comparisons.radix [in Float.Fcomp]
comparisons.radixMoreThanOne [in Float.Fcomp]
comparisons.radixMoreThanZERO [in Float.Fcomp]


D

definitions.radix [in Float.Float]
definitions.radixMoreThanOne [in Float.Float]
definitions.radixMoreThanZERO [in Float.Float]


F

Fbounded_Def.FtoRradix [in Float.Fbound]
Fbounded_Def.radixMoreThanZERO [in Float.Fbound]
Fbounded_Def.radixMoreThanOne [in Float.Fbound]
Fbounded_Def.radix [in Float.Fbound]
Fclosestp2.b [in Float.ClosestProp]
Fclosestp2.FtoRradix [in Float.ClosestProp]
Fclosestp2.pGivesBound [in Float.ClosestProp]
Fclosestp2.precision [in Float.ClosestProp]
Fclosestp2.precisionGreaterThanOne [in Float.ClosestProp]
Fclosestp2.radix [in Float.ClosestProp]
Fclosestp2.radixMoreThanOne [in Float.ClosestProp]
Fclosestp2.radixMoreThanZERO [in Float.ClosestProp]
Fclosest.b [in Float.Closest]
Fclosest.FtoRradix [in Float.Closest]
Fclosest.pGivesBound [in Float.Closest]
Fclosest.precision [in Float.Closest]
Fclosest.precisionGreaterThanOne [in Float.Closest]
Fclosest.radix [in Float.Closest]
Fclosest.radixMoreThanOne [in Float.Closest]
finduct.b [in Float.Finduct]
finduct.FtoRradix [in Float.Finduct]
finduct.pGivesBound [in Float.Finduct]
finduct.precision [in Float.Finduct]
finduct.precisionNotZero [in Float.Finduct]
finduct.radix [in Float.Finduct]
finduct.radixMoreThanOne [in Float.Finduct]
finduct.radixMoreThanZERO [in Float.Finduct]
FMinMax.b [in Float.Fmin]
FMinMax.FtoRradix [in Float.Fmin]
FMinMax.pGivesBound [in Float.Fmin]
FMinMax.precision [in Float.Fmin]
FMinMax.precisionNotZero [in Float.Fmin]
FMinMax.radix [in Float.Fmin]
FMinMax.radixMoreThanOne [in Float.Fmin]
FMinMax.radixMoreThanZERO [in Float.Fmin]
Fnormalized_Def.pGivesBound [in Float.Fnorm]
Fnormalized_Def.precisionNotZero [in Float.Fnorm]
Fnormalized_Def.precision [in Float.Fnorm]
Fnormalized_Def.b [in Float.Fnorm]
Fnormalized_Def.FtoRradix [in Float.Fnorm]
Fnormalized_Def.radixMoreThanZERO [in Float.Fnorm]
Fnormalized_Def.radixMoreThanOne [in Float.Fnorm]
Fnormalized_Def.radix [in Float.Fnorm]
FOdd.b [in Float.Fodd]
FOdd.FtoRradix [in Float.Fodd]
FOdd.pGivesBound [in Float.Fodd]
FOdd.precision [in Float.Fodd]
FOdd.precisionGreaterThanOne [in Float.Fodd]
FOdd.radix [in Float.Fodd]
FOdd.radixMoreThanOne [in Float.Fodd]
FOdd.radixMoreThanZERO [in Float.Fodd]
Fprop.b [in Float.Fprop]
Fprop.FtoRradix [in Float.Fprop]
Fprop.radix [in Float.Fprop]
Fprop.radixMoreThanOne [in Float.Fprop]
FRoundP.b [in Float.FroundProp]
FRoundP.b [in Float.FroundMult]
FRoundP.b [in Float.FroundPlus]
FRoundP.b [in Float.ClosestMult]
FRoundP.FtoRradix [in Float.FroundProp]
FRoundP.FtoRradix [in Float.FroundMult]
FRoundP.FtoRradix [in Float.FroundPlus]
FRoundP.FtoRradix [in Float.ClosestMult]
FRoundP.pGivesBound [in Float.FroundProp]
FRoundP.pGivesBound [in Float.FroundMult]
FRoundP.pGivesBound [in Float.FroundPlus]
FRoundP.pGivesBound [in Float.ClosestMult]
FRoundP.precision [in Float.FroundProp]
FRoundP.precision [in Float.FroundMult]
FRoundP.precision [in Float.FroundPlus]
FRoundP.precision [in Float.ClosestMult]
FRoundP.precisionGreaterThanOne [in Float.FroundProp]
FRoundP.precisionGreaterThanOne [in Float.FroundMult]
FRoundP.precisionGreaterThanOne [in Float.FroundPlus]
FRoundP.precisionGreaterThanOne [in Float.ClosestMult]
FRoundP.radix [in Float.FroundProp]
FRoundP.radix [in Float.FroundMult]
FRoundP.radix [in Float.FroundPlus]
FRoundP.radix [in Float.ClosestMult]
FRoundP.radixMoreThanOne [in Float.FroundProp]
FRoundP.radixMoreThanOne [in Float.FroundMult]
FRoundP.radixMoreThanOne [in Float.FroundPlus]
FRoundP.radixMoreThanOne [in Float.ClosestMult]
FRoundP.radixMoreThanZERO [in Float.FroundProp]
FRoundP.radixMoreThanZERO [in Float.FroundMult]
FRoundP.radixMoreThanZERO [in Float.FroundPlus]
FRound.b [in Float.Fround]
FRound.FtoRradix [in Float.Fround]
FRound.pGivesBound [in Float.Fround]
FRound.precision [in Float.Fround]
FRound.precisionGreaterThanOne [in Float.Fround]
FRound.radix [in Float.Fround]
FRound.radixMoreThanOne [in Float.Fround]
F2.b [in Float.Closest2Plus]
F2.b [in Float.Closest2Prop]
F2.FtoRradix [in Float.Closest2Plus]
F2.FtoRradix [in Float.Closest2Prop]
F2.pGivesBound [in Float.Closest2Plus]
F2.pGivesBound [in Float.Closest2Prop]
F2.precision [in Float.Closest2Plus]
F2.precision [in Float.Closest2Prop]
F2.precisionNotZero [in Float.Closest2Plus]
F2.precisionNotZero [in Float.Closest2Prop]
F2.radix [in Float.Closest2Plus]
F2.radix [in Float.Closest2Prop]


M

mf.FtoRradix [in Float.MSB]
mf.radix [in Float.MSB]
mf.radixMoreThanOne [in Float.MSB]
mf.radixMoreThanZERO [in Float.MSB]
MSBProp.b [in Float.MSBProp]
MSBProp.FtoRradix [in Float.MSBProp]
MSBProp.pGivesBound [in Float.MSBProp]
MSBProp.precision [in Float.MSBProp]
MSBProp.precisionGreaterThanOne [in Float.MSBProp]
MSBProp.radix [in Float.MSBProp]
MSBProp.radixMoreThanOne [in Float.MSBProp]
MSBProp.radixMoreThanZERO [in Float.MSBProp]


O

operations.FtoRradix [in Float.Fop]
operations.radix [in Float.Fop]
operations.radixNotZero [in Float.Fop]


P

Pdigit.n [in Float.Digit]
Pdigit.nMoreThanOne [in Float.Digit]
Pdigit.nMoreThan1 [in Float.Digit]
pred.b [in Float.FPred]
pred.FtoRradix [in Float.FPred]
pred.pGivesBound [in Float.FPred]
pred.precision [in Float.FPred]
pred.precisionNotZero [in Float.FPred]
pred.radix [in Float.FPred]
pred.radixMoreThanOne [in Float.FPred]


S

suc.b [in Float.FSucc]
suc.FtoRradix [in Float.FSucc]
suc.pGivesBound [in Float.FSucc]
suc.precision [in Float.FSucc]
suc.precisionNotZero [in Float.FSucc]
suc.radix [in Float.FSucc]
suc.radixMoreThanOne [in Float.FSucc]
suc.radixMoreThanZERO [in Float.FSucc]
suc1.b [in Float.FSucc]
suc1.FtoRradix [in Float.FSucc]
suc1.pGivesBound [in Float.FSucc]
suc1.precision [in Float.FSucc]
suc1.precisionNotZero [in Float.FSucc]
suc1.radix [in Float.FSucc]
suc1.radixMoreThanOne [in Float.FSucc]



Library Index

A

AllFloat


C

Closest
ClosestMult
ClosestPlus
ClosestProp
Closest2Plus
Closest2Prop


D

Digit


F

Faux
Fbound
Fcomp
Finduct
Float
Fmin
Fnorm
Fodd
Fop
FPred
Fprop
Fround
FroundMult
FroundPlus
FroundProp
FSucc


M

MSB
MSBProp


O

Option


P

Paux
Power


R

Rpow


S

sTactic


Z

Zdivides
Zenum



Lemma Index

A

absFBounded [in Float.Fbound]
absolu_lt_nz [in Float.Faux]
absolu_Zs_neg [in Float.Faux]
absolu_Zs [in Float.Faux]
absolu_comp_mult [in Float.Faux]
absolu_Zopp [in Float.Faux]
absolu_INR [in Float.Faux]
abs_lt_MSB [in Float.MSB]
AScal2 [in Float.Closest2Prop]


B

BminusSameExp [in Float.Fprop]
BminusSameExpAux [in Float.Fprop]
BminusSameExpNeg [in Float.Fprop]
boundBoundNat [in Float.Fmin]
boundedNorMinGivesExp [in Float.Fnorm]
boundNatCorrect [in Float.Fmin]
boundNormalMult [in Float.MSBProp]
boundOnePrecision [in Float.MSBProp]
boundRCorrect1 [in Float.Fmin]
boundRCorrect2 [in Float.Fmin]
boundRrOpp [in Float.Fmin]


C

CanonicFulp [in Float.FroundProp]
ClosestCompatible [in Float.Closest]
ClosestErrorBound [in Float.ClosestProp]
ClosestErrorBoundNormal [in Float.ClosestProp]
ClosestErrorBoundNormal_aux [in Float.ClosestProp]
ClosestErrorBoundNormal2_aux [in Float.ClosestProp]
ClosestErrorBound2 [in Float.ClosestProp]
ClosestErrorExp [in Float.ClosestProp]
ClosestErrorExpStrict [in Float.ClosestProp]
ClosestExp [in Float.ClosestProp]
ClosestFabs [in Float.ClosestProp]
ClosestIdem [in Float.ClosestProp]
closestLessMultAbs [in Float.ClosestMult]
closestLessMultNeg [in Float.ClosestMult]
closestLessMultPos [in Float.ClosestMult]
ClosestMax [in Float.Closest]
ClosestMaxEq [in Float.Closest]
ClosestMin [in Float.Closest]
ClosestMinEq [in Float.Closest]
ClosestMinOrMax [in Float.Closest]
ClosestMonotone [in Float.Closest]
ClosestM1 [in Float.ClosestProp]
ClosestOpp [in Float.ClosestProp]
ClosestPropHigham25 [in Float.ClosestProp]
ClosestRoundedModeP [in Float.Closest]
ClosestSymmetric [in Float.Closest]
ClosestTotal [in Float.Closest]
ClosestUlp [in Float.ClosestProp]
compare_SUP_dec [in Float.Paux]
Contradict1 [in Float.sTactic]
Contradict2 [in Float.sTactic]
Contradict3 [in Float.sTactic]
convert_not_O [in Float.Faux]


D

digitAdd [in Float.Digit]
digitAuxLess [in Float.Digit]
digitAuxMore [in Float.Digit]
digitAux1 [in Float.Digit]
digitGivesBoundedNum [in Float.Fnorm]
digitInv [in Float.Digit]
digitLess [in Float.Digit]
digitMore [in Float.Digit]
digitnNormMin [in Float.Fnorm]
digitNotZero [in Float.Digit]
digitO [in Float.Digit]
digitPredVNumiSPrecision [in Float.Fnorm]
digitVNumiSPrecision [in Float.Fnorm]
digit_anti_monotone_lt [in Float.Digit]
digit_abs [in Float.Digit]
digit_bound [in Float.Digit]
digit_minus1 [in Float.Digit]
digit_monotone [in Float.Digit]
digit1 [in Float.Digit]
div2IsBetween [in Float.FroundProp]
div2IsBetweenPos [in Float.FroundProp]


E

eqExpLess [in Float.Fbound]
eqExpMax [in Float.Fbound]
errorBoundedMult [in Float.FroundMult]
errorBoundedMultClosest [in Float.ClosestMult]
errorBoundedMultClosest_aux [in Float.ClosestMult]
errorBoundedMultExp [in Float.FroundMult]
errorBoundedMultExpPos [in Float.FroundMult]
errorBoundedMultExp_aux [in Float.FroundMult]
errorBoundedMultMax [in Float.FroundMult]
errorBoundedMultMin [in Float.FroundMult]
errorBoundedMultNeg [in Float.FroundMult]
errorBoundedMultPos [in Float.FroundMult]
errorBoundedPlus [in Float.ClosestPlus]
errorBoundedPlusAbs [in Float.ClosestPlus]
errorBoundedPlusLe [in Float.ClosestPlus]
EvenClosestCompatible [in Float.Closest]
EvenClosestMinOrMax [in Float.Closest]
EvenClosestMonotone [in Float.Closest]
EvenClosestRoundedModeP [in Float.Closest]
EvenClosestSymmetric [in Float.Closest]
EvenClosestTotal [in Float.Closest]
EvenClosestUniqueP [in Float.Closest]
EvenExp [in Float.Fodd]
EvenFNSuccFNSuccMid [in Float.Closest2Prop]
EvenMultInv [in Float.Fodd]
EvenMult1 [in Float.Fodd]
EvenMult2 [in Float.Fodd]
EvenNOdd [in Float.Fodd]
EvenO [in Float.Fodd]
EvenOpp [in Float.Fodd]
EvenPlusInv1 [in Float.Fodd]
EvenPlusInv2 [in Float.Fodd]
EvenPlus1 [in Float.Fodd]
EvenPlus2 [in Float.Fodd]
EvenSOdd [in Float.Fodd]
EvenSOddInv [in Float.Fodd]
ExactMinusInterval [in Float.FroundPlus]
ExactMinusIntervalAux [in Float.FroundPlus]
ExactMinusIntervalAux1 [in Float.FroundPlus]
expPlus [in Float.Paux]


F

Fabs_Fzero [in Float.Fop]
Fabs_correct [in Float.Fop]
Fabs_correct2 [in Float.Fop]
Fabs_correct1 [in Float.Fop]
FboundedEqExp [in Float.Fbound]
FboundedEqExpPos [in Float.Fbound]
FboundedExp [in Float.Fbound]
FboundedFzero [in Float.Fbound]
FboundedMbound [in Float.Fnorm]
FboundedMboundPos [in Float.Fnorm]
FboundedNum [in Float.Fbound]
FboundedOne [in Float.Fnorm]
FBoundedPred [in Float.FPred]
FBoundedScale [in Float.Fbound]
FboundedShiftLess [in Float.Fbound]
FBoundedSuc [in Float.FSucc]
FboundedZeroSameExp [in Float.Fbound]
FboundNext [in Float.Fnorm]
FcanonicBound [in Float.Fnorm]
FcanonicFabs [in Float.Fnorm]
FcanonicFnormalizeEq [in Float.Fnorm]
FcanonicFopp [in Float.Fnorm]
FcanonicLeastExp [in Float.Fnorm]
FcanonicLePos [in Float.Fnorm]
FcanonicLtNeg [in Float.Fnorm]
FcanonicLtPos [in Float.Fnorm]
FcanonicNegFexpRlt [in Float.Fnorm]
FcanonicNnormMin [in Float.Fnorm]
FcanonicPosFexpRlt [in Float.Fnorm]
FcanonicPpred [in Float.Fnorm]
FcanonicUnique [in Float.Fnorm]
Fcanonic_Rle_Zle [in Float.Fnorm]
Fdiff_correct [in Float.Fcomp]
FdigitEq [in Float.Float]
Fdigit_abs [in Float.Fop]
Fdigit_opp [in Float.Fop]
Feq_bool_correct_f [in Float.Fcomp]
Feq_bool_correct_r [in Float.Fcomp]
Feq_bool_correct_t [in Float.Fcomp]
FEvenD [in Float.Fodd]
FevenFop [in Float.Fodd]
FevenNormMin [in Float.Closest2Prop]
FevenO [in Float.Fodd]
FevenOrFodd [in Float.Fodd]
FevenPred [in Float.Fodd]
FevenSuc [in Float.Fodd]
FevenSucProp [in Float.Fodd]
Fexp_le_MSB [in Float.MSB]
Fexp_le_LSB [in Float.MSB]
Fge_Zge [in Float.Fcomp]
Fgt_Zgt [in Float.Fcomp]
FinductNeg [in Float.Finduct]
FinductNegAux [in Float.Finduct]
FinductPos [in Float.Finduct]
FinductPosAux [in Float.Finduct]
firstNormalPosNormal [in Float.Fnorm]
Fle_trans [in Float.Fcomp]
Fle_refl [in Float.Fcomp]
Fle_Fge [in Float.Fcomp]
Fle_Zle [in Float.Fcomp]
Fle_bool_correct_f [in Float.Fcomp]
Fle_bool_correct_r [in Float.Fcomp]
Fle_bool_correct_t [in Float.Fcomp]
floatDec [in Float.Float]
floatEq [in Float.Float]
Flt_Fgt [in Float.Fcomp]
Flt_Zlt [in Float.Fcomp]
Flt_bool_correct_f [in Float.Fcomp]
Flt_bool_correct_r [in Float.Fcomp]
Flt_bool_correct_t [in Float.Fcomp]
FmaxRep [in Float.Fmin]
FminRep [in Float.Fmin]
Fminus_correct [in Float.Fop]
FmultRadixInv [in Float.ClosestProp]
FNEvenD [in Float.Fodd]
FNevenEq [in Float.Fodd]
FNevenFop [in Float.Fodd]
FNevenOrFNodd [in Float.Fodd]
FNevenPred [in Float.Fodd]
FNevenSuc [in Float.Fodd]
FNoddEq [in Float.Fodd]
FNoddFop [in Float.Fodd]
FnOddNEven [in Float.Fodd]
FNoddPred [in Float.Fodd]
FNoddSuc [in Float.Fodd]
FnormalBound [in Float.Fnorm]
FnormalBoundAbs [in Float.Fnorm]
FnormalBoundAbs2 [in Float.Fnorm]
FnormalBounded [in Float.Fnorm]
FnormalFabs [in Float.Fnorm]
FnormalFop [in Float.Fnorm]
FnormalizeBounded [in Float.Fnorm]
FnormalizeCanonic [in Float.Fnorm]
FnormalizeCorrect [in Float.Fnorm]
Fnormalize_Fopp [in Float.Fnorm]
FnormalLtFirstNormalNeg [in Float.Fnorm]
FnormalLtFirstNormalPos [in Float.Fnorm]
FnormalLtNeg [in Float.Fnorm]
FnormalLtPos [in Float.Fnorm]
FnormalNnormMin [in Float.Fnorm]
FnormalNotZero [in Float.Fnorm]
FnormalPpred [in Float.Fnorm]
FnormalPrecision [in Float.Fnorm]
FnormalUnique [in Float.Fnorm]
FNPredCanonic [in Float.FPred]
FNPredFopFNSucc [in Float.FPred]
FNPredLt [in Float.FPred]
FNPredProp [in Float.FPred]
FNPredSuc [in Float.FPred]
FNPredSucEq [in Float.FPred]
FNSuccCanonic [in Float.FSucc]
FNSuccEq [in Float.FSucc]
FNSuccFNSuccMid [in Float.FSucc]
FNSuccLt [in Float.FSucc]
FNSuccProp [in Float.FSucc]
FNSuccUlpPos [in Float.FroundProp]
FNSucPred [in Float.FPred]
FNSucPredEq [in Float.FPred]
FoddFop [in Float.Fodd]
FoddPred [in Float.Fodd]
FoddSuc [in Float.Fodd]
Fopp_Fminus_dist [in Float.Fop]
Fopp_Fminus [in Float.Fop]
Fopp_Fopp [in Float.Fop]
Fopp_correct [in Float.Fop]
FopRepAux [in Float.Fbound]
Fplus_correct [in Float.Fop]
FPredCanonic [in Float.FPred]
FPredDiff1 [in Float.FPred]
FPredDiff2 [in Float.FPred]
FPredDiff3 [in Float.FPred]
FPredFopFSucc [in Float.FPred]
FPredLt [in Float.FPred]
FPredProp [in Float.FPred]
FPredSimpl1 [in Float.FPred]
FPredSimpl2 [in Float.FPred]
FPredSimpl3 [in Float.FPred]
FPredSimpl4 [in Float.FPred]
FPredSuc [in Float.FPred]
FpredUlpPos [in Float.ClosestProp]
FPredZleEq [in Float.FPred]
FshiftAdd [in Float.Float]
FshiftCorrect [in Float.Float]
FshiftCorrectInv [in Float.Float]
FshiftCorrectSym [in Float.Float]
FshiftFdigit [in Float.Float]
FshiftO [in Float.Float]
FsubnormalBound [in Float.Fnorm]
FsubnormalDigit [in Float.Fnorm]
FsubnormalFbounded [in Float.Fnorm]
FsubnormalFexp [in Float.Fnorm]
FsubnormalLt [in Float.Fnorm]
FsubnormalLtFirstNormalPos [in Float.Fnorm]
FsubnormalnormalLtNeg [in Float.Fnorm]
FsubnormalnormalLtPos [in Float.Fnorm]
FsubnormalUnique [in Float.Fnorm]
FsubnormFabs [in Float.Fnorm]
FsubnormFopp [in Float.Fnorm]
FSuccCanonic [in Float.FSucc]
FSuccDiffPos [in Float.FroundProp]
FSuccDiff1 [in Float.FSucc]
FSuccDiff2 [in Float.FSucc]
FSuccDiff3 [in Float.FSucc]
FSuccLt [in Float.FSucc]
FSuccNegCanonic [in Float.FSucc]
FSuccNormNegNormMin [in Float.FSucc]
FSuccNormNegNotNormMin [in Float.FSucc]
FSuccNormPos [in Float.FSucc]
FSuccPosNotMax [in Float.FSucc]
FSuccProp [in Float.FSucc]
FSuccPropNeg [in Float.FSucc]
FSuccPropPos [in Float.FSucc]
FSuccSimpl1 [in Float.FSucc]
FSuccSimpl2 [in Float.FSucc]
FSuccSimpl3 [in Float.FSucc]
FSuccSimpl4 [in Float.FSucc]
FSuccSubnormal [in Float.FSucc]
FSuccSubnormNearNormMin [in Float.FSucc]
FSuccSubnormNotNearNormMin [in Float.FSucc]
FSuccUlpPos [in Float.FroundProp]
FSuccZleEq [in Float.FSucc]
FSucFSucMid [in Float.FSucc]
FSucPred [in Float.FPred]
FtoREqInv1 [in Float.Float]
FtoREqInv2 [in Float.Float]
FulpComp [in Float.FroundProp]
FulpFabs [in Float.FroundProp]
FulpFPredGePos [in Float.FroundProp]
FulpFPredLe [in Float.ClosestProp]
FulpGe [in Float.FroundProp]
FulpLe [in Float.FroundProp]
FulpLe2 [in Float.FroundProp]
FulpPred [in Float.FroundProp]
FulpPredCan [in Float.FroundProp]
FulpSuc [in Float.FroundProp]
FulpSucCan [in Float.FroundProp]
FUlp_Le_LSigB [in Float.FroundProp]
Fulp_zero [in Float.FroundProp]
FvalScale [in Float.Fbound]
FweightEq [in Float.Finduct]
FweightLt [in Float.Finduct]
FweightZle [in Float.Finduct]
FzeroisReallyZero [in Float.Float]
FzeroisZero [in Float.Fbound]
Fzero_opp [in Float.Fop]


I

InBinade [in Float.FroundProp]
inject_nat_eq [in Float.Faux]
inject_nat_convert [in Float.Faux]
inj_pred [in Float.Faux]
inj_abs [in Float.Faux]
inj_oZ1 [in Float.Zdivides]
INR_inv [in Float.Faux]
INR_lt_nm [in Float.Faux]
Int_part_IZR [in Float.Faux]
Int_part_INR [in Float.Faux]
in_map_inv [in Float.Zenum]
isBounded [in Float.Fbound]
isMaxComp [in Float.FroundProp]
isMax_inv1 [in Float.Fmin]
isMinComp [in Float.FroundProp]
isMin_inv1 [in Float.Fmin]
is_Fzero_rep2 [in Float.Float]
is_Fzero_rep1 [in Float.Float]
is_FzeroP [in Float.Float]
IZR_inv [in Float.Faux]
IZR_zero_r [in Float.Faux]
IZR_zero [in Float.Faux]


L

LeFnumZERO [in Float.Fcomp]
LeFulpPos [in Float.FroundProp]
LeR0Fnum [in Float.Fcomp]
LessExpBound [in Float.Fbound]
LeZEROFnum [in Float.Fcomp]
le_Rle [in Float.Faux]
le_mult_anti_compatibility [in Float.Faux]
le_next [in Float.Faux]
le_refl_eq [in Float.Faux]
LSBMinus [in Float.FroundPlus]
LSBPlus [in Float.FroundPlus]
LSB_rep_min [in Float.MSB]
LSB_rep [in Float.MSB]
LSB_le_abs [in Float.MSB]
LSB_le_MSB [in Float.MSB]
LSB_abs [in Float.MSB]
LSB_opp [in Float.MSB]
LSB_comp [in Float.MSB]
LSB_shift [in Float.MSB]
lte_comp_mult [in Float.Faux]
LtFnumZERO [in Float.Float]
LtFsubnormal [in Float.Fnorm]
LtR0Fnum [in Float.Fcomp]
lt_S_le [in Float.Faux]
lt_Zlt_inv [in Float.Faux]
lt_Rlt [in Float.Faux]
lt_mult_anti_compatibility [in Float.Faux]
lt_minus_inv [in Float.Faux]
lt_next [in Float.Faux]
lt_comp_mult [in Float.Faux]
lt_comp_mult_r [in Float.Faux]
lt_comp_mult_l [in Float.Faux]
lt_le_pred [in Float.Faux]


M

MaxBinade [in Float.Fmin]
MaxCompatible [in Float.Fround]
maxDivCorrect [in Float.MSB]
maxDivLess [in Float.MSB]
maxDivLt [in Float.MSB]
maxDivPlus [in Float.MSB]
maxDivSimpl [in Float.MSB]
maxDivSimplAux [in Float.MSB]
maxDivSimplInv [in Float.MSB]
maxDivSimplInvAux [in Float.MSB]
maxDivUnique [in Float.MSB]
maxDivUniqueDigit [in Float.MSB]
maxDivUniqueInverse [in Float.MSB]
maxDivUniqueInverseDigit [in Float.MSB]
maxDiv_abs [in Float.MSB]
maxDiv_opp [in Float.MSB]
MaxEq [in Float.Fmin]
MaxEx [in Float.Fmin]
maxFbounded [in Float.Fbound]
MaxFloat [in Float.Fnorm]
maxMax [in Float.Fbound]
maxMaxBis [in Float.Fnorm]
maxMax1 [in Float.Fnorm]
MaxMin [in Float.Fmin]
MaxOppMin [in Float.Fmin]
MaxRoundedModeP [in Float.Fround]
MaxUniqueP [in Float.Fround]
mBFadic_correct4 [in Float.Fmin]
mBFadic_correct3 [in Float.Fmin]
mBFadic_correct2 [in Float.Fmin]
mBFadic_correct1 [in Float.Fmin]
mBPadic_Fbounded [in Float.Fmin]
MinBinade [in Float.Fmin]
MinCompatible [in Float.Fround]
MinEq [in Float.Fmin]
MinEx [in Float.Fmin]
MinExList [in Float.Fmin]
MinMax [in Float.Fmin]
MinOppMax [in Float.Fmin]
MinOrMaxRep [in Float.Fround]
MinRoundedModeP [in Float.Fround]
MinUniqueP [in Float.Fround]
minusRoundRep [in Float.FroundPlus]
minusSameExp [in Float.Fop]
minus_le [in Float.Faux]
minus_inv_lt [in Float.Faux]
minus_inv_lt_aux [in Float.Faux]
minus_minus [in Float.Faux]
min_n_0 [in Float.Faux]
min_or [in Float.Faux]
MonotoneMax [in Float.Fmin]
MonotoneMin [in Float.Fmin]
mProd_correct_rev2 [in Float.Zenum]
mProd_correct_rev1 [in Float.Zenum]
mProd_correct [in Float.Zenum]
MSBBoundNotZero [in Float.FroundProp]
MSBisMin [in Float.FroundProp]
MSBroundLSB [in Float.FroundPlus]
MSBtoZero [in Float.FroundProp]
MSB_mix [in Float.MSB]
MSB_le_mult [in Float.MSB]
MSB_le_multAux [in Float.MSB]
MSB_monotone [in Float.MSB]
MSB_monotoneAux [in Float.MSB]
MSB_le_abs [in Float.MSB]
MSB_abs [in Float.MSB]
MSB_opp [in Float.MSB]
MSB_comp [in Float.MSB]
MSB_shift [in Float.MSB]
multExpMin [in Float.FroundMult]
multExpUpperBound [in Float.FroundMult]
mult_eq_inv [in Float.Faux]
mult_le_MSB [in Float.MSB]
mult_le_MSBAux [in Float.MSB]
mZlist_correct_rev2 [in Float.Zenum]
mZlist_correct_rev1 [in Float.Zenum]
mZlist_correct [in Float.Zenum]
mZlist_aux_correct_rev2 [in Float.Zenum]
mZlist_aux_correct_rev1 [in Float.Zenum]
mZlist_aux_correct [in Float.Zenum]


N

NconvertO [in Float.Faux]
NDivides_minus [in Float.Zdivides]
NEq_IZRO [in Float.Faux]
NEq_INR1 [in Float.Faux]
NEq_INRO [in Float.Faux]
NEq_INR [in Float.Faux]
NisFzeroComp [in Float.Float]
nNormMimLtvNum [in Float.FSucc]
nNormPos [in Float.Fnorm]
nNrMMimLevNum [in Float.Fnorm]
NormalAndSubNormalNotEq [in Float.Fnorm]
NormalNotSubNormal [in Float.Fnorm]
NotDividesDigit [in Float.Zdivides]
notEqLt [in Float.Faux]
NotZmultZero [in Float.Faux]
not_O_lt [in Float.Faux]
NroundN [in Float.FroundProp]


O

OddEvenDec [in Float.Fodd]
OddExp [in Float.Fodd]
OddMult [in Float.Fodd]
OddMultInv [in Float.Fodd]
OddNEven [in Float.Fodd]
OddOpp [in Float.Fodd]
OddPlusInv1 [in Float.Fodd]
OddPlusInv2 [in Float.Fodd]
OddPlus1 [in Float.Fodd]
OddPlus2 [in Float.Fodd]
OddSEven [in Float.Fodd]
OddSEvenInv [in Float.Fodd]
odd_even_lem [in Float.Paux]
Odd1 [in Float.Fodd]
oneExp_Zle [in Float.Float]
oneExp_Zlt [in Float.Float]
oneExp_lt [in Float.Float]
oneExp_le [in Float.Float]
oneZplus [in Float.Fop]
oppBounded [in Float.Fbound]
oppBoundedInv [in Float.Fbound]


P

PdivBound_correct4 [in Float.Paux]
PdivBound_correct3 [in Float.Paux]
PdivBound_correct2 [in Float.Paux]
PdivBound_correct1 [in Float.Paux]
PdivBound_correct [in Float.Paux]
Pdivless_correct [in Float.Paux]
Pdivless1 [in Float.Paux]
Pdivless2 [in Float.Paux]
Pdiv_correct [in Float.Paux]
pGivesDigit [in Float.Fnorm]
plusClosestLowerBound [in Float.Closest2Plus]
plusClosestLowerBoundAux1 [in Float.Closest2Plus]
plusClosestLowerBoundAux2 [in Float.Closest2Plus]
plusErrorBound1 [in Float.ClosestPlus]
plusErrorBound1bis [in Float.ClosestPlus]
plusErrorBound1withZero [in Float.ClosestPlus]
plusErrorBound2 [in Float.Closest2Plus]
plusExactExp [in Float.ClosestPlus]
plusExactExpCanonic [in Float.ClosestPlus]
plusExactR0 [in Float.ClosestPlus]
plusExact1 [in Float.ClosestPlus]
plusExact1bis [in Float.ClosestPlus]
plusExact2 [in Float.ClosestPlus]
plusExact2Aux [in Float.ClosestPlus]
plusExpBound [in Float.FroundPlus]
plusExpMin [in Float.FroundPlus]
plusExpUpperBound [in Float.FroundPlus]
plusUpperBound [in Float.Closest2Plus]
PminPos [in Float.FroundProp]
pNormal_absolu_min [in Float.Fnorm]
positive_exp_correct [in Float.Paux]
PosNormMin [in Float.Fnorm]
pos_eq_bool_correct [in Float.Faux]
pos_length_pow [in Float.Digit]
powerRZ_R1 [in Float.Power]
powerRZ_le [in Float.Power]
powerRZ_lt [in Float.Power]
powerRZ_Zs [in Float.Power]
powerRZ_Zopp [in Float.Power]
powerRZ_add [in Float.Power]
powerRZ_NOR [in Float.Power]
powerRZ_1 [in Float.Power]
powerRZ_O [in Float.Power]
powerRZ_R1 [in Float.Rpow]
powerRZ_le [in Float.Rpow]
powerRZ_lt [in Float.Rpow]
powerRZ_Zs [in Float.Rpow]
powerRZ_Zopp [in Float.Rpow]
powerRZ_add [in Float.Rpow]
powerRZ_NOR [in Float.Rpow]
powerRZ_1 [in Float.Rpow]
powerRZ_O [in Float.Rpow]
pow_R1 [in Float.Power]
pow_lt [in Float.Power]
pow_RN_plus [in Float.Power]
pow_add [in Float.Power]
pow_NR0 [in Float.Power]
pow_1 [in Float.Power]
pow_O [in Float.Power]
pow_R1 [in Float.Rpow]
pow_lt [in Float.Rpow]
pow_RN_plus [in Float.Rpow]
pow_add [in Float.Rpow]
pow_NR0 [in Float.Rpow]
pow_1 [in Float.Rpow]
pow_O [in Float.Rpow]
pPredMoreThanOne [in Float.ClosestPlus]
pPredMoreThanRadix [in Float.ClosestPlus]
ProjectMax [in Float.Fmin]
ProjectMin [in Float.Fmin]
pSubnormal_absolu_min [in Float.Fnorm]
ptonat_def1 [in Float.Faux]
pUCanonic_absolu [in Float.Fnorm]


R

Rabsolu_Zabs [in Float.Faux]
Rabsolu_left1 [in Float.Faux]
radixRangeBoundExp [in Float.Finduct]
radixRangeBoundExp [in Float.FroundPlus]
ReqGivesEqwithSameExp [in Float.Float]
Rinv_powerRZ [in Float.Rpow]
RleBoundRoundl [in Float.FroundProp]
RleBoundRoundr [in Float.FroundProp]
Rledouble [in Float.Faux]
RleFexpFabs [in Float.Fop]
RleMaxR0 [in Float.FroundProp]
RleMinR0 [in Float.FroundProp]
RleRoundedLessR0 [in Float.FroundProp]
RleRoundedR0 [in Float.FroundProp]
Rle_Rinv [in Float.Faux]
Rle_INR [in Float.Faux]
Rle_IZR1 [in Float.Faux]
Rle_IZRO [in Float.Faux]
Rle_IZR [in Float.Faux]
Rle_R0_Ropp [in Float.Faux]
Rle_powerRZ [in Float.Power]
Rle_Float_Zle [in Float.Float]
Rle_monotony_contra_exp [in Float.Float]
Rle_monotone_exp [in Float.Float]
Rle_powerRZ [in Float.Rpow]
Rle_Fexp_eq_Zle [in Float.Fcomp]
RlIt2 [in Float.Faux]
Rltdouble [in Float.Faux]
Rlt_RinvDouble [in Float.Faux]
Rlt_IZR1 [in Float.Faux]
Rlt_IZRO [in Float.Faux]
Rlt_IZR [in Float.Faux]
Rlt_INR1 [in Float.Faux]
Rlt_R0_Ropp [in Float.Faux]
Rlt_Rminus_ZERO [in Float.Faux]
Rlt_powerRZ [in Float.Power]
Rlt_pow [in Float.Power]
Rlt_pow_R1 [in Float.Power]
Rlt_Float_Zlt [in Float.Float]
Rlt_monotony_contra_exp [in Float.Float]
Rlt_monotony_exp [in Float.Float]
Rlt_powerRZ [in Float.Rpow]
Rlt_pow [in Float.Rpow]
Rlt_pow_R1 [in Float.Rpow]
Rlt_Fexp_eq_Zlt [in Float.Fcomp]
Rlt2 [in Float.Faux]
RmaxAbs [in Float.Faux]
RmaxLess1 [in Float.Faux]
RmaxLess2 [in Float.Faux]
RmaxRmult [in Float.Faux]
RmaxSym [in Float.Faux]
Rmult_IZR [in Float.Faux]
RoundAbsMonotonel [in Float.FroundProp]
RoundAbsMonotoner [in Float.FroundProp]
RoundBound [in Float.ClosestPlus]
roundedModeAbsMult [in Float.FroundProp]
RoundedModeBounded [in Float.FroundProp]
RoundedModeErrorExpStrict [in Float.FroundProp]
roundedModeLessMult [in Float.FroundProp]
roundedModeMoreMult [in Float.FroundProp]
RoundedModeMult [in Float.FroundProp]
RoundedModeMultAbs [in Float.FroundProp]
RoundedModeMultLess [in Float.FroundProp]
RoundedModeProjectorIdem [in Float.FroundProp]
RoundedModeProjectorIdemEq [in Float.FroundProp]
RoundedModeP_inv4 [in Float.Fround]
RoundedModeP_inv3 [in Float.Fround]
RoundedModeP_inv2 [in Float.Fround]
RoundedModeP_inv1 [in Float.Fround]
RoundedModeRep [in Float.Fround]
RoundedModeUlp [in Float.FroundProp]
RoundedProjector [in Float.Fround]
RoundLessThanIsMax [in Float.Fround]
RoundLSBMax [in Float.FroundProp]
RoundMSBmax [in Float.FroundProp]
RoundMSBmin [in Float.FroundProp]
Rpow_eq_inv [in Float.Power]
Rpow_R1 [in Float.Power]
Rpow_eq_inv [in Float.Rpow]
Rpow_R1 [in Float.Rpow]
R0LeFnum [in Float.Fcomp]
R0LtFnum [in Float.Fcomp]
R0RltRlePred [in Float.FPred]
R0RltRleSucc [in Float.FSucc]


S

sameExpEq [in Float.Float]
ScalableRoundedModeP [in Float.Fround]
Sterbenz [in Float.Fprop]
SterbenzAux [in Float.Fprop]


T

ToInfinityCompatible [in Float.Fround]
ToInfinityMinOrMax [in Float.Fround]
ToInfinityMonotone [in Float.Fround]
ToInfinityRoundedModeP [in Float.Fround]
ToInfinitySymmetric [in Float.Fround]
ToInfinityTotal [in Float.Fround]
ToInfinityUniqueP [in Float.Fround]
ToZeroCompatible [in Float.Fround]
ToZeroMinOrMax [in Float.Fround]
ToZeroMonotone [in Float.Fround]
ToZeroRoundedModeP [in Float.Fround]
ToZeroSymmetric [in Float.Fround]
ToZeroTotal [in Float.Fround]
ToZeroUniqueP [in Float.Fround]
TwoMoreThanOne [in Float.Closest2Plus]
TwoMoreThanOne [in Float.Closest2Prop]


U

Ulp_Le_LSigB [in Float.MSB]


V

vNumbMoreThanOne [in Float.Fnorm]
vNumPrecision [in Float.Fnorm]


Z

Zabs_intro [in Float.Faux]
Zabs_Zopp [in Float.Faux]
Zabs_Zs [in Float.Faux]
Zabs_eq_opp [in Float.Faux]
Zabs_Zmult [in Float.Faux]
Zabs_absolu [in Float.Faux]
Zabs_tri [in Float.Zdivides]
Zabs_eq_case [in Float.Zdivides]
Zcompare_EGAL [in Float.Faux]
Zcompare_correct [in Float.Digit]
ZdividesDiv [in Float.Zdivides]
ZDividesLe [in Float.Zdivides]
ZdividesLessPow [in Float.Zdivides]
ZdividesMult [in Float.Zdivides]
ZdividesTrans [in Float.Zdivides]
ZdividesZquotient [in Float.Zdivides]
ZdividesZquotientInv [in Float.Zdivides]
ZDivides_mult [in Float.Zdivides]
ZDivides_add [in Float.Zdivides]
Zdivides1 [in Float.Zdivides]
Zeq_Zs [in Float.Faux]
Zeq_mult_simpl [in Float.Zdivides]
Zero_le_oZ [in Float.Zdivides]
ZleAbs [in Float.Faux]
ZleLe [in Float.Faux]
Zle_Zpred_inv [in Float.Faux]
Zle_Zpred_Zlt [in Float.Faux]
Zle_n_Zpred [in Float.Faux]
Zle_Zabs_inv2 [in Float.Faux]
Zle_Zabs_inv1 [in Float.Faux]
Zle_ZERO_Zabs [in Float.Faux]
Zle_Zpred_Zpred [in Float.Faux]
Zle_Zminus_ZERO [in Float.Faux]
Zle_Zabs [in Float.Faux]
Zle_Zpred [in Float.Faux]
Zle_Rle [in Float.Faux]
Zle_abs [in Float.Faux]
Zle_Zopp_Inv [in Float.Faux]
Zle_next [in Float.Faux]
Zle_Zmult_comp_l [in Float.Faux]
Zle_Zmult_comp_r [in Float.Faux]
Zle_mult_gen [in Float.Faux]
Zle_Zopp [in Float.Faux]
Zle_monotony_contra_abs_pow [in Float.Fbound]
Zle_powerRZ [in Float.Rpow]
ZltNormMinVnum [in Float.FSucc]
Zlt_Zabs_intro [in Float.Faux]
Zlt_ZERO_Zle_ONE [in Float.Faux]
Zlt_not_eq_rev [in Float.Faux]
Zlt_not_eq [in Float.Faux]
Zlt_1_O [in Float.Faux]
Zlt_Zabs_Zpred [in Float.Faux]
Zlt_Zabs_inv2 [in Float.Faux]
Zlt_Zabs_inv1 [in Float.Faux]
Zlt_Zminus_ZERO [in Float.Faux]
Zlt_mult_ZERO [in Float.Faux]
Zlt_mult_simpl_l [in Float.Faux]
Zlt_Rlt [in Float.Faux]
Zlt_absolu [in Float.Faux]
Zlt_Zopp_Inv [in Float.Faux]
Zlt_next [in Float.Faux]
Zlt_Zopp [in Float.Faux]
Zlt_powerRZ [in Float.Power]
Zlt_powerRZ [in Float.Rpow]
ZmaxLe1 [in Float.Faux]
ZmaxLe2 [in Float.Faux]
ZmaxSym [in Float.Faux]
Zmax_le1 [in Float.Faux]
Zmax_le2 [in Float.Faux]
Zminus_n_predm [in Float.Faux]
Zmin_Zmax [in Float.Faux]
Zmin_Zle [in Float.Faux]
Zmin_le2 [in Float.Faux]
Zmin_le1 [in Float.Faux]
Zmin_sym [in Float.Faux]
Zopp_Zpred_Zs [in Float.Faux]
Zpower_nat_1 [in Float.Faux]
Zpower_nat_O [in Float.Faux]
Zpower_nat_powerRZ_absolu [in Float.Power]
Zpower_nat_powerRZ [in Float.Power]
Zpower_NR1 [in Float.Power]
Zpower_NR0 [in Float.Power]
Zpower_nat_powerRZ_absolu [in Float.Rpow]
Zpower_nat_Z_powerRZ [in Float.Rpow]
Zpower_NR1 [in Float.Rpow]
Zpower_NR0 [in Float.Rpow]
Zpower_nat_anti_eq [in Float.Digit]
Zpower_nat_anti_monotone_le [in Float.Digit]
Zpower_nat_monotone_le [in Float.Digit]
Zpower_nat_anti_monotone_lt [in Float.Digit]
Zpower_nat_monotone_lt [in Float.Digit]
Zpower_nat_monotone_S [in Float.Digit]
Zpower_nat_less [in Float.Digit]
Zpred_Zle_Zabs_intro [in Float.Faux]
Zpred_Zopp_Zs [in Float.Faux]
ZquotientMonotone [in Float.Zdivides]
ZquotientPos [in Float.Zdivides]
ZquotientProp [in Float.Zdivides]
ZquotientUnique [in Float.Zdivides]
ZquotientZopp [in Float.Zdivides]
Zquotient_mult_comp [in Float.Zdivides]
Zquotient1 [in Float.Zdivides]
ZroundZ [in Float.FroundProp]
Z_eq_bool_correct [in Float.Faux]
Z_O_1 [in Float.Faux]



Constructor Index

B

Bound [in Float.Fbound]


F

Float [in Float.Float]


N

None [in Float.Option]


S

Some [in Float.Option]



Projection Index

D

dExp [in Float.Fbound]


F

Fexp [in Float.Float]
Fnum [in Float.Float]


V

vNum [in Float.Fbound]



Inductive Index

O

Option [in Float.Option]



Section Index

B

bugFix [in Float.Paux]


C

ClosestP [in Float.ClosestPlus]
comparisons [in Float.Fcomp]


D

definitions [in Float.Float]


F

Fbounded_Def [in Float.Fbound]
Fclosest [in Float.Closest]
Fclosestp2 [in Float.ClosestProp]
finduct [in Float.Finduct]
FMinMax [in Float.Fmin]
Fnormalized_Def [in Float.Fnorm]
FOdd [in Float.Fodd]
Fprop [in Float.Fprop]
FRound [in Float.Fround]
FRoundP [in Float.FroundProp]
FRoundP [in Float.FroundMult]
FRoundP [in Float.FroundPlus]
FRoundP [in Float.ClosestMult]
F2 [in Float.Closest2Plus]
F2 [in Float.Closest2Prop]


M

mf [in Float.MSB]
MSBProp [in Float.MSBProp]


O

operations [in Float.Fop]


P

Pdigit [in Float.Digit]
pred [in Float.FPred]


S

suc [in Float.FSucc]
suc1 [in Float.FSucc]



Definition Index

B

boundNat [in Float.Fmin]
boundR [in Float.Fmin]


C

Closest [in Float.Closest]
CompatibleP [in Float.Fround]


D

digit [in Float.Digit]
digitAux [in Float.Digit]


E

Even [in Float.Fodd]
EvenClosest [in Float.Closest]
exp [in Float.Paux]


F

Fabs [in Float.Fop]
Fbounded [in Float.Fbound]
Fcanonic [in Float.Fnorm]
Fcompare [in Float.Fcomp]
Fdiff [in Float.Fcomp]
Fdigit [in Float.Float]
Feq [in Float.Fcomp]
Feq_bool [in Float.Fcomp]
Feven [in Float.Fodd]
Fge [in Float.Fcomp]
Fgt [in Float.Fcomp]
firstNormalPos [in Float.Fnorm]
Fle [in Float.Fcomp]
Fle_bool [in Float.Fcomp]
Flt [in Float.Fcomp]
Flt_bool [in Float.Fcomp]
Fminus [in Float.Fop]
Fmult [in Float.Fop]
Fmult_correct [in Float.Fop]
FNeven [in Float.Fodd]
FNodd [in Float.Fodd]
Fnormal [in Float.Fnorm]
Fnormalize [in Float.Fnorm]
FNPred [in Float.FPred]
FNSucc [in Float.FSucc]
Fodd [in Float.Fodd]
Fopp [in Float.Fop]
Fplus [in Float.Fop]
FPred [in Float.FPred]
Fshift [in Float.Float]
Fsubnormal [in Float.Fnorm]
FSucc [in Float.FSucc]
FtoR [in Float.Float]
Fulp [in Float.FroundProp]
Fweight [in Float.Finduct]
Fzero [in Float.Float]


I

isMax [in Float.Fmin]
isMin [in Float.Fmin]
is_Fzero [in Float.Float]


L

LSB [in Float.MSB]


M

maxDiv [in Float.MSB]
mBFloat [in Float.Fmin]
MinOrMaxP [in Float.Fround]
MonotoneP [in Float.Fmin]
mProd [in Float.Zenum]
MSB [in Float.MSB]
mZlist [in Float.Zenum]
mZlist_aux [in Float.Zenum]


N

natEq [in Float.Faux]
nNormMin [in Float.Fnorm]


O

Odd [in Float.Fodd]
oZ [in Float.Paux]
oZ1 [in Float.Zdivides]


P

Pdiv [in Float.Paux]
PdivBound [in Float.Paux]
Pdivless [in Float.Paux]
PdivlessAux [in Float.Paux]
positive_exp [in Float.Paux]
pos_eq_bool [in Float.Faux]
pos_length [in Float.Digit]
powerRZ [in Float.Power]
pPred [in Float.Fnorm]
ProjectorP [in Float.Fmin]


R

RoundedModeP [in Float.Fround]


S

SymmetricP [in Float.Fround]


T

ToInfinityP [in Float.Fround]
TotalP [in Float.Fround]
ToZeroP [in Float.Fround]


U

UniqueP [in Float.Fround]


Z

Zdivides [in Float.Zdivides]
ZdividesP [in Float.Zdivides]
Zmax [in Float.Faux]
Zquotient [in Float.Zdivides]
Z_eq_bool [in Float.Faux]



Record Index

F

Fbound [in Float.Fbound]
float [in Float.Float]



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 (1091 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 (161 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 (33 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 (777 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 (4 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 (4 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 (1 entry)
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 (26 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 (83 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 (2 entries)

This page has been generated by coqdoc