Sophie

Sophie

distrib > Mageia > 6 > armv5tl > media > core-release > by-pkgid > 3c7997fe0e8405f6d7b5563e63d17a78 > files > 104

coq-flocq-2.5.1-2.mga6.armv5tl.rpm

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<title>Table of contents</title>
</head>

<body>

<div id="page">

<div id="header">
</div>

<div id="main">

<div id="toc">
<a href="Flocq.Flocq_version.html"><h2>Library Flocq.Flocq_version</h2></a>
<a href="Flocq.Core.Fcore_Raux.html"><h2>Library Flocq.Core.Fcore_Raux</h2></a>
<ul class="doclist">
<li><a href="Flocq.Core.Fcore_Raux.html#lab1">Missing definitions/lemmas</a>

</li>
</ul>
<a href="Flocq.Core.Fcore_Zaux.html"><h2>Library Flocq.Core.Fcore_Zaux</h2></a>
<a href="Flocq.Core.Fcore_defs.html"><h2>Library Flocq.Core.Fcore_defs</h2></a>
<ul class="doclist">
<li><a href="Flocq.Core.Fcore_defs.html#lab2">Basic definitions: float and rounding property</a>

</li>
</ul>
<a href="Flocq.Core.Fcore_digits.html"><h2>Library Flocq.Core.Fcore_digits</h2></a>
<a href="Flocq.Core.Fcore_float_prop.html"><h2>Library Flocq.Core.Fcore_float_prop</h2></a>
<ul class="doclist">
<li><a href="Flocq.Core.Fcore_float_prop.html#lab3">Basic properties of floating-point formats: lemmas about mantissa, exponent...</a>

</li>
</ul>
<a href="Flocq.Core.Fcore_FIX.html"><h2>Library Flocq.Core.Fcore_FIX</h2></a>
<ul class="doclist">
<li><a href="Flocq.Core.Fcore_FIX.html#lab4">Fixed-point format</a>

</li>
</ul>
<a href="Flocq.Core.Fcore_FLT.html"><h2>Library Flocq.Core.Fcore_FLT</h2></a>
<ul class="doclist">
<li><a href="Flocq.Core.Fcore_FLT.html#lab5">Floating-point format with gradual underflow</a>

</li>
</ul>
<a href="Flocq.Core.Fcore_FLX.html"><h2>Library Flocq.Core.Fcore_FLX</h2></a>
<ul class="doclist">
<li><a href="Flocq.Core.Fcore_FLX.html#lab6">Floating-point format without underflow</a>

</li>
</ul>
<a href="Flocq.Core.Fcore_FTZ.html"><h2>Library Flocq.Core.Fcore_FTZ</h2></a>
<ul class="doclist">
<li><a href="Flocq.Core.Fcore_FTZ.html#lab7">Floating-point format with abrupt underflow</a>

</li>
</ul>
<a href="Flocq.Core.Fcore_generic_fmt.html"><h2>Library Flocq.Core.Fcore_generic_fmt</h2></a>
<ul class="doclist">
<li><a href="Flocq.Core.Fcore_generic_fmt.html#lab8">What is a real number belonging to a format, and many properties.</a>

</li>
</ul>
<a href="Flocq.Core.Fcore_rnd.html"><h2>Library Flocq.Core.Fcore_rnd</h2></a>
<ul class="doclist">
<li><a href="Flocq.Core.Fcore_rnd.html#lab9">Roundings: properties and/or functions</a>

</li>
</ul>
<a href="Flocq.Core.Fcore_rnd_ne.html"><h2>Library Flocq.Core.Fcore_rnd_ne</h2></a>
<ul class="doclist">
<li><a href="Flocq.Core.Fcore_rnd_ne.html#lab10">Rounding to nearest, ties to even: existence, unicity...</a>

</li>
</ul>
<a href="Flocq.Core.Fcore_ulp.html"><h2>Library Flocq.Core.Fcore_ulp</h2></a>
<ul class="doclist">
<li><a href="Flocq.Core.Fcore_ulp.html#lab11">Unit in the Last Place: our definition using fexp and its properties, successor and predecessor</a>

</li>
</ul>
<a href="Flocq.Core.Fcore.html"><h2>Library Flocq.Core.Fcore</h2></a>
<a href="Flocq.Calc.Fcalc_bracket.html"><h2>Library Flocq.Calc.Fcalc_bracket</h2></a>
<ul class="doclist">
<li><a href="Flocq.Calc.Fcalc_bracket.html#lab12">Locations: where a real number is positioned with respect to its rounded-down value in an arbitrary format.</a>

</li>
</ul>
<a href="Flocq.Calc.Fcalc_digits.html"><h2>Library Flocq.Calc.Fcalc_digits</h2></a>
<ul class="doclist">
<li><a href="Flocq.Calc.Fcalc_digits.html#lab13">Functions for computing the number of digits of integers and related theorems.</a>

</li>
</ul>
<a href="Flocq.Calc.Fcalc_div.html"><h2>Library Flocq.Calc.Fcalc_div</h2></a>
<ul class="doclist">
<li><a href="Flocq.Calc.Fcalc_div.html#lab14">Helper function and theorem for computing the rounded quotient of two floating-point numbers.</a>

</li>
</ul>
<a href="Flocq.Calc.Fcalc_ops.html"><h2>Library Flocq.Calc.Fcalc_ops</h2></a>
<a href="Flocq.Calc.Fcalc_round.html"><h2>Library Flocq.Calc.Fcalc_round</h2></a>
<ul class="doclist">
<li><a href="Flocq.Calc.Fcalc_round.html#lab15">Helper function for computing the rounded value of a real number.</a>

</li>
<li><a href="Flocq.Calc.Fcalc_round.html#lab16">Instances of the theorems above, for the usual rounding modes.</a>

</li>
</ul>
<a href="Flocq.Calc.Fcalc_sqrt.html"><h2>Library Flocq.Calc.Fcalc_sqrt</h2></a>
<ul class="doclist">
<li><a href="Flocq.Calc.Fcalc_sqrt.html#lab17">Helper functions and theorems for computing the rounded square root of a floating-point number.</a>

</li>
</ul>
<a href="Flocq.Prop.Fprop_div_sqrt_error.html"><h2>Library Flocq.Prop.Fprop_div_sqrt_error</h2></a>
<ul class="doclist">
<li><a href="Flocq.Prop.Fprop_div_sqrt_error.html#lab18">Remainder of the division and square root are in the FLX format</a>

</li>
</ul>
<a href="Flocq.Prop.Fprop_mult_error.html"><h2>Library Flocq.Prop.Fprop_mult_error</h2></a>
<ul class="doclist">
<li><a href="Flocq.Prop.Fprop_mult_error.html#lab19">Error of the multiplication is in the FLX/FLT format</a>

</li>
</ul>
<a href="Flocq.Prop.Fprop_plus_error.html"><h2>Library Flocq.Prop.Fprop_plus_error</h2></a>
<ul class="doclist">
<li><a href="Flocq.Prop.Fprop_plus_error.html#lab20">Error of the rounded-to-nearest addition is representable.</a>

</li>
</ul>
<a href="Flocq.Prop.Fprop_relative.html"><h2>Library Flocq.Prop.Fprop_relative</h2></a>
<ul class="doclist">
<li><a href="Flocq.Prop.Fprop_relative.html#lab21">Relative error of the roundings</a>

</li>
</ul>
<a href="Flocq.Prop.Fprop_Sterbenz.html"><h2>Library Flocq.Prop.Fprop_Sterbenz</h2></a>
<ul class="doclist">
<li><a href="Flocq.Prop.Fprop_Sterbenz.html#lab22">Sterbenz conditions for exact subtraction</a>

</li>
</ul>
<a href="Flocq.Appli.Fappli_rnd_odd.html"><h2>Library Flocq.Appli.Fappli_rnd_odd</h2></a>
<ul class="doclist">
<li><a href="Flocq.Appli.Fappli_rnd_odd.html#lab23">Rounding to odd and its properties, including the equivalence</a>

</li>
</ul>
<a href="Flocq.Appli.Fappli_IEEE.html"><h2>Library Flocq.Appli.Fappli_IEEE</h2></a>
<ul class="doclist">
<li><a href="Flocq.Appli.Fappli_IEEE.html#lab24">IEEE-754 arithmetic</a>

</li>
</ul>
<a href="Flocq.Appli.Fappli_IEEE_bits.html"><h2>Library Flocq.Appli.Fappli_IEEE_bits</h2></a>
<ul class="doclist">
<li><a href="Flocq.Appli.Fappli_IEEE_bits.html#lab25">IEEE-754 encoding of binary floating-point data</a>

</li>
</ul>
<a href="Flocq.Appli.Fappli_double_round.html"><h2>Library Flocq.Appli.Fappli_double_round</h2></a>
<ul class="doclist">
<li><a href="Flocq.Appli.Fappli_double_round.html#lab26">Conditions for innocuous double rounding.</a>

</li>
</ul>
</div>
<hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>

</div>

</body>
</html>

Perl :: Catalyst :: PostgreSQL :: RPM Valid HTML 4.01 Transitional