<!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>Flocq.Appli.Fappli_IEEE_bits</title> </head> <body> <div id="page"> <div id="header"> </div> <div id="main"> <h1 class="libtitle">Library Flocq.Appli.Fappli_IEEE_bits</h1> <div class="code"> </div> <div class="doc"> This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ <div class="paragraph"> </div> Copyright (C) 2011-2013 Sylvie Boldo <br /> Copyright (C) 2011-2013 Guillaume Melquiond <div class="paragraph"> </div> This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version. <div class="paragraph"> </div> This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details. <div class="paragraph"> </div> <a name="lab25"></a><h1 class="section">IEEE-754 encoding of binary floating-point data</h1> </div> <div class="code"> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore.html#"><span class="id" title="library">Fcore</span></a>.<br/> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#"><span class="id" title="library">Fcore_digits</span></a>.<br/> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Calc.Fcalc_digits.html#"><span class="id" title="library">Fcalc_digits</span></a>.<br/> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#"><span class="id" title="library">Fappli_IEEE</span></a>.<br/> <br/> <span class="id" title="keyword">Section</span> <a name="Binary_Bits"><span class="id" title="section">Binary_Bits</span></a>.<br/> <br/> <span class="id" title="keyword">Implicit Arguments</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#exist"><span class="id" title="constructor">exist</span></a> [[<span class="id" title="var">A</span>] [<span class="id" title="var">P</span>]].<br/> <span class="id" title="keyword">Implicit Arguments</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_zero"><span class="id" title="constructor">B754_zero</span></a> [[<span class="id" title="var">prec</span>] [<span class="id" title="var">emax</span>]].<br/> <span class="id" title="keyword">Implicit Arguments</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_infinity"><span class="id" title="constructor">B754_infinity</span></a> [[<span class="id" title="var">prec</span>] [<span class="id" title="var">emax</span>]].<br/> <span class="id" title="keyword">Implicit Arguments</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_nan"><span class="id" title="constructor">B754_nan</span></a> [[<span class="id" title="var">prec</span>] [<span class="id" title="var">emax</span>]].<br/> <span class="id" title="keyword">Implicit Arguments</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_finite"><span class="id" title="constructor">B754_finite</span></a> [[<span class="id" title="var">prec</span>] [<span class="id" title="var">emax</span>]].<br/> <br/> </div> <div class="doc"> Number of bits for the fraction and exponent </div> <div class="code"> <span class="id" title="keyword">Variable</span> <a name="Binary_Bits.mw"><span class="id" title="variable">mw</span></a> <a name="Binary_Bits.ew"><span class="id" title="variable">ew</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/> <span class="id" title="keyword">Hypothesis</span> <a name="Binary_Bits.Hmw"><span class="id" title="variable">Hmw</span></a> : (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a>)%<span class="id" title="var">Z</span>.<br/> <span class="id" title="keyword">Hypothesis</span> <a name="Binary_Bits.Hew"><span class="id" title="variable">Hew</span></a> : (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a>)%<span class="id" title="var">Z</span>.<br/> <br/> <span class="id" title="keyword">Let</span> <a name="Binary_Bits.emax"><span class="id" title="variable">emax</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 (<a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1).<br/> <span class="id" title="keyword">Let</span> <a name="Binary_Bits.prec"><span class="id" title="variable">prec</span></a> := (<a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1)%<span class="id" title="var">Z</span>.<br/> <span class="id" title="keyword">Let</span> <a name="Binary_Bits.emin"><span class="id" title="variable">emin</span></a> := (3 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.emax"><span class="id" title="variable">emax</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.prec"><span class="id" title="variable">prec</span></a>)%<span class="id" title="var">Z</span>.<br/> <span class="id" title="keyword">Let</span> <a name="Binary_Bits.binary_float"><span class="id" title="variable">binary_float</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#binary_float"><span class="id" title="inductive">binary_float</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.emax"><span class="id" title="variable">emax</span></a>.<br/> <br/> <span class="id" title="keyword">Let</span> <a name="Binary_Bits.Hprec"><span class="id" title="variable">Hprec</span></a> : (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.prec"><span class="id" title="variable">prec</span></a>)%<span class="id" title="var">Z</span>.<br/> <span class="id" title="keyword">Qed</span>.<br/> <br/> <span class="id" title="keyword">Let</span> <a name="Binary_Bits.Hm_gt_0"><span class="id" title="variable">Hm_gt_0</span></a> : (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> 2<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#186f1fc9207177b1a4e8373ac9655977"><span class="id" title="notation">^</span></a><a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a>)%<span class="id" title="var">Z</span>.<br/> <span class="id" title="keyword">Qed</span>.<br/> <br/> <span class="id" title="keyword">Let</span> <a name="Binary_Bits.He_gt_0"><span class="id" title="variable">He_gt_0</span></a> : (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> 2<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#186f1fc9207177b1a4e8373ac9655977"><span class="id" title="notation">^</span></a><a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a>)%<span class="id" title="var">Z</span>.<br/> <span class="id" title="keyword">Qed</span>.<br/> <br/> <span class="id" title="keyword">Hypothesis</span> <a name="Binary_Bits.Hmax"><span class="id" title="variable">Hmax</span></a> : (<a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.emax"><span class="id" title="variable">emax</span></a>)%<span class="id" title="var">Z</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="join_bits"><span class="id" title="definition">join_bits</span></a> (<span class="id" title="var">s</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>) <span class="id" title="var">m</span> <span class="id" title="var">e</span> :=<br/> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.shiftl"><span class="id" title="definition">Z.shiftl</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">(</span></a><span class="id" title="keyword">if</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#s"><span class="id" title="variable">s</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a> <span class="id" title="keyword">else</span> 0<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#e"><span class="id" title="variable">e</span></a>) <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#m"><span class="id" title="variable">m</span></a>)%<span class="id" title="var">Z</span>.<br/> <br/> <span class="id" title="keyword">Lemma</span> <a name="join_bits_range"><span class="id" title="lemma">join_bits_range</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">s</span> <span class="id" title="var">m</span> <span class="id" title="var">e</span>,<br/> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> 2<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#186f1fc9207177b1a4e8373ac9655977"><span class="id" title="notation">^</span></a><a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> 2<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#186f1fc9207177b1a4e8373ac9655977"><span class="id" title="notation">^</span></a><a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#join_bits"><span class="id" title="definition">join_bits</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> 2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#186f1fc9207177b1a4e8373ac9655977"><span class="id" title="notation">^</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#186f1fc9207177b1a4e8373ac9655977"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#186f1fc9207177b1a4e8373ac9655977"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">Z</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="split_bits"><span class="id" title="definition">split_bits</span></a> <span class="id" title="var">x</span> :=<br/> <span class="id" title="keyword">let</span> <span class="id" title="var">mm</span> := <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a> <span class="id" title="keyword">in</span><br/> <span class="id" title="keyword">let</span> <span class="id" title="var">em</span> := <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a> <span class="id" title="keyword">in</span><br/> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zle_bool"><span class="id" title="abbreviation">Zle_bool</span></a> (<a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#mm"><span class="id" title="variable">mm</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#em"><span class="id" title="variable">em</span></a>) <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zmod"><span class="id" title="abbreviation">Zmod</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#mm"><span class="id" title="variable">mm</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zmod"><span class="id" title="abbreviation">Zmod</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zdiv"><span class="id" title="abbreviation">Zdiv</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#mm"><span class="id" title="variable">mm</span></a>) <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#em"><span class="id" title="variable">em</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">Z</span>.<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="split_join_bits"><span class="id" title="lemma">split_join_bits</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">s</span> <span class="id" title="var">m</span> <span class="id" title="var">e</span>,<br/> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#split_bits"><span class="id" title="definition">split_bits</span></a> (<a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#join_bits"><span class="id" title="definition">join_bits</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#e"><span class="id" title="variable">e</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="join_split_bits"><span class="id" title="lemma">join_split_bits</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 (<a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> <span class="id" title="keyword">let</span> '<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">s</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">m</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">e</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#split_bits"><span class="id" title="definition">split_bits</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">in</span><br/> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#join_bits"><span class="id" title="definition">join_bits</span></a> <span class="id" title="var">s</span> <span class="id" title="var">m</span> <span class="id" title="var">e</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a>.<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="split_bits_inj"><span class="id" title="lemma">split_bits_inj</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 (<a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 (<a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#split_bits"><span class="id" title="definition">split_bits</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#split_bits"><span class="id" title="definition">split_bits</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#y"><span class="id" title="variable">y</span></a>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="bits_of_binary_float"><span class="id" title="definition">bits_of_binary_float</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.binary_float"><span class="id" title="variable">binary_float</span></a>) :=<br/> <span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/> | <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_zero"><span class="id" title="constructor">B754_zero</span></a> <span class="id" title="var">sx</span> ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#join_bits"><span class="id" title="definition">join_bits</span></a> <span class="id" title="var">sx</span> 0 0<br/> | <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_infinity"><span class="id" title="constructor">B754_infinity</span></a> <span class="id" title="var">sx</span> ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#join_bits"><span class="id" title="definition">join_bits</span></a> <span class="id" title="var">sx</span> 0 (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1)<br/> | <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_nan"><span class="id" title="constructor">B754_nan</span></a> <span class="id" title="var">sx</span> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#exist"><span class="id" title="constructor">exist</span></a> <span class="id" title="var">plx</span> <span class="id" title="var">_</span>) ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#join_bits"><span class="id" title="definition">join_bits</span></a> <span class="id" title="var">sx</span> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">plx</span>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1)<br/> | <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_finite"><span class="id" title="constructor">B754_finite</span></a> <span class="id" title="var">sx</span> <span class="id" title="var">mx</span> <span class="id" title="var">ex</span> <span class="id" title="var">_</span> ⇒<br/> <span class="id" title="keyword">let</span> <span class="id" title="var">m</span> := (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">mx</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a>)%<span class="id" title="var">Z</span> <span class="id" title="keyword">in</span><br/> <span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zle_bool"><span class="id" title="abbreviation">Zle_bool</span></a> 0 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#m"><span class="id" title="variable">m</span></a> <span class="id" title="keyword">then</span><br/> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#join_bits"><span class="id" title="definition">join_bits</span></a> <span class="id" title="var">sx</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#m"><span class="id" title="variable">m</span></a> (<span class="id" title="var">ex</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1)<br/> <span class="id" title="keyword">else</span><br/> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#join_bits"><span class="id" title="definition">join_bits</span></a> <span class="id" title="var">sx</span> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">mx</span>) 0<br/> <span class="id" title="keyword">end</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="split_bits_of_binary_float"><span class="id" title="definition">split_bits_of_binary_float</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.binary_float"><span class="id" title="variable">binary_float</span></a>) :=<br/> <span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/> | <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_zero"><span class="id" title="constructor">B754_zero</span></a> <span class="id" title="var">sx</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">sx</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">Z</span><br/> | <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_infinity"><span class="id" title="constructor">B754_infinity</span></a> <span class="id" title="var">sx</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">sx</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">Z</span><br/> | <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_nan"><span class="id" title="constructor">B754_nan</span></a> <span class="id" title="var">sx</span> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#exist"><span class="id" title="constructor">exist</span></a> <span class="id" title="var">plx</span> <span class="id" title="var">_</span>) ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">sx</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">plx</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">Z</span><br/> | <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_finite"><span class="id" title="constructor">B754_finite</span></a> <span class="id" title="var">sx</span> <span class="id" title="var">mx</span> <span class="id" title="var">ex</span> <span class="id" title="var">_</span> ⇒<br/> <span class="id" title="keyword">let</span> <span class="id" title="var">m</span> := (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">mx</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a>)%<span class="id" title="var">Z</span> <span class="id" title="keyword">in</span><br/> <span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zle_bool"><span class="id" title="abbreviation">Zle_bool</span></a> 0 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#m"><span class="id" title="variable">m</span></a> <span class="id" title="keyword">then</span><br/> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">sx</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">ex</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">Z</span><br/> <span class="id" title="keyword">else</span><br/> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">sx</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">mx</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">Z</span><br/> <span class="id" title="keyword">end</span>.<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="split_bits_of_binary_float_correct"><span class="id" title="lemma">split_bits_of_binary_float_correct</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#split_bits"><span class="id" title="definition">split_bits</span></a> (<a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#bits_of_binary_float"><span class="id" title="definition">bits_of_binary_float</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#split_bits_of_binary_float"><span class="id" title="definition">split_bits_of_binary_float</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a>.<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="bits_of_binary_float_range"><span class="id" title="lemma">bits_of_binary_float_range</span></a>:<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#bits_of_binary_float"><span class="id" title="definition">bits_of_binary_float</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> 2<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#186f1fc9207177b1a4e8373ac9655977"><span class="id" title="notation">^(</span></a><a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a><a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a>1<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#186f1fc9207177b1a4e8373ac9655977"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">Z</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="binary_float_of_bits_aux"><span class="id" title="definition">binary_float_of_bits_aux</span></a> <span class="id" title="var">x</span> :=<br/> <span class="id" title="keyword">let</span> '<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">sx</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">mx</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">ex</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#split_bits"><span class="id" title="definition">split_bits</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">in</span><br/> <span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zeq_bool"><span class="id" title="definition">Zeq_bool</span></a> <span class="id" title="var">ex</span> 0 <span class="id" title="keyword">then</span><br/> <span class="id" title="keyword">match</span> <span class="id" title="var">mx</span> <span class="id" title="keyword">with</span><br/> | <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a> ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#F754_zero"><span class="id" title="constructor">F754_zero</span></a> <span class="id" title="var">sx</span><br/> | <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">px</span> ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#F754_finite"><span class="id" title="constructor">F754_finite</span></a> <span class="id" title="var">sx</span> <span class="id" title="var">px</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.emin"><span class="id" title="variable">emin</span></a><br/> | <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zneg"><span class="id" title="constructor">Zneg</span></a> <span class="id" title="var">_</span> ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#F754_nan"><span class="id" title="constructor">F754_nan</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xH"><span class="id" title="constructor">xH</span></a> <br/> <span class="id" title="keyword">end</span><br/> <span class="id" title="keyword">else</span> <span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zeq_bool"><span class="id" title="definition">Zeq_bool</span></a> <span class="id" title="var">ex</span> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1) <span class="id" title="keyword">then</span><br/> <span class="id" title="keyword">match</span> <span class="id" title="var">mx</span> <span class="id" title="keyword">with</span><br/> | <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a> ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#F754_infinity"><span class="id" title="constructor">F754_infinity</span></a> <span class="id" title="var">sx</span><br/> | <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">plx</span> ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#F754_nan"><span class="id" title="constructor">F754_nan</span></a> <span class="id" title="var">sx</span> <span class="id" title="var">plx</span><br/> | <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zneg"><span class="id" title="constructor">Zneg</span></a> <span class="id" title="var">_</span> ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#F754_nan"><span class="id" title="constructor">F754_nan</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xH"><span class="id" title="constructor">xH</span></a> <br/> <span class="id" title="keyword">end</span><br/> <span class="id" title="keyword">else</span><br/> <span class="id" title="keyword">match</span> (<span class="id" title="var">mx</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> 2 <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a>)%<span class="id" title="var">Z</span> <span class="id" title="keyword">with</span><br/> | <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">px</span> ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#F754_finite"><span class="id" title="constructor">F754_finite</span></a> <span class="id" title="var">sx</span> <span class="id" title="var">px</span> (<span class="id" title="var">ex</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1)<br/> | <span class="id" title="var">_</span> ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#F754_nan"><span class="id" title="constructor">F754_nan</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xH"><span class="id" title="constructor">xH</span></a> <br/> <span class="id" title="keyword">end</span>.<br/> <br/> <span class="id" title="keyword">Lemma</span> <a name="binary_float_of_bits_aux_correct"><span class="id" title="lemma">binary_float_of_bits_aux_correct</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#valid_binary"><span class="id" title="definition">valid_binary</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.emax"><span class="id" title="variable">emax</span></a> (<a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binary_float_of_bits_aux"><span class="id" title="definition">binary_float_of_bits_aux</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="binary_float_of_bits"><span class="id" title="definition">binary_float_of_bits</span></a> <span class="id" title="var">x</span> :=<br/> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#FF2B"><span class="id" title="definition">FF2B</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.emax"><span class="id" title="variable">emax</span></a> <span class="id" title="var">_</span> (<a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binary_float_of_bits_aux_correct"><span class="id" title="lemma">binary_float_of_bits_aux_correct</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a>).<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="binary_float_of_bits_of_binary_float"><span class="id" title="lemma">binary_float_of_bits_of_binary_float</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binary_float_of_bits"><span class="id" title="definition">binary_float_of_bits</span></a> (<a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#bits_of_binary_float"><span class="id" title="definition">bits_of_binary_float</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a>.<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="bits_of_binary_float_of_bits"><span class="id" title="lemma">bits_of_binary_float_of_bits</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> 2<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#186f1fc9207177b1a4e8373ac9655977"><span class="id" title="notation">^(</span></a><a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.mw"><span class="id" title="variable">mw</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a><a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits.ew"><span class="id" title="variable">ew</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a>1<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#186f1fc9207177b1a4e8373ac9655977"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#bits_of_binary_float"><span class="id" title="definition">bits_of_binary_float</span></a> (<a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binary_float_of_bits"><span class="id" title="definition">binary_float_of_bits</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#x"><span class="id" title="variable">x</span></a>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#Binary_Bits"><span class="id" title="section">Binary_Bits</span></a>.<br/> <br/> </div> <div class="doc"> Specialization for IEEE single precision operations </div> <div class="code"> <span class="id" title="keyword">Section</span> <a name="B32_Bits"><span class="id" title="section">B32_Bits</span></a>.<br/> <br/> <span class="id" title="keyword">Implicit Arguments</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_nan"><span class="id" title="constructor">B754_nan</span></a> [[<span class="id" title="var">prec</span>] [<span class="id" title="var">emax</span>]].<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="binary32"><span class="id" title="definition">binary32</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#binary_float"><span class="id" title="inductive">binary_float</span></a> 24 128.<br/> <br/> <span class="id" title="keyword">Let</span> <a name="B32_Bits.Hprec"><span class="id" title="variable">Hprec</span></a> : (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> 24)%<span class="id" title="var">Z</span>.<br/> <span class="id" title="keyword">Qed</span>.<br/> <br/> <span class="id" title="keyword">Let</span> <a name="B32_Bits.Hprec_emax"><span class="id" title="variable">Hprec_emax</span></a> : (24 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> 128)%<span class="id" title="var">Z</span>.<br/> <span class="id" title="keyword">Qed</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="default_nan_pl32"><span class="id" title="definition">default_nan_pl32</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#nan_pl"><span class="id" title="definition">nan_pl</span></a> 24 :=<br/> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#exist"><span class="id" title="constructor">exist</span></a> <span class="id" title="var">_</span> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#iter_nat"><span class="id" title="definition">iter_nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xO"><span class="id" title="constructor">xO</span></a> 22 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xH"><span class="id" title="constructor">xH</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#refl_equal"><span class="id" title="abbreviation">refl_equal</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="unop_nan_pl32"><span class="id" title="definition">unop_nan_pl32</span></a> (<span class="id" title="var">f</span> : <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binary32"><span class="id" title="definition">binary32</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#nan_pl"><span class="id" title="definition">nan_pl</span></a> 24 :=<br/> <span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#f"><span class="id" title="variable">f</span></a> <span class="id" title="keyword">with</span><br/> | <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_nan"><span class="id" title="constructor">B754_nan</span></a> <span class="id" title="var">s</span> <span class="id" title="var">pl</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">s</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">pl</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/> | <span class="id" title="var">_</span> ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#default_nan_pl32"><span class="id" title="definition">default_nan_pl32</span></a><br/> <span class="id" title="keyword">end</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="binop_nan_pl32"><span class="id" title="definition">binop_nan_pl32</span></a> (<span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binary32"><span class="id" title="definition">binary32</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#nan_pl"><span class="id" title="definition">nan_pl</span></a> 24 :=<br/> <span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#f1"><span class="id" title="variable">f1</span></a>, <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#f2"><span class="id" title="variable">f2</span></a> <span class="id" title="keyword">with</span><br/> | <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_nan"><span class="id" title="constructor">B754_nan</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">pl1</span>, <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">s1</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">pl1</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/> | <span class="id" title="var">_</span>, <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_nan"><span class="id" title="constructor">B754_nan</span></a> <span class="id" title="var">s2</span> <span class="id" title="var">pl2</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">s2</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">pl2</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/> | <span class="id" title="var">_</span>, <span class="id" title="var">_</span> ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#default_nan_pl32"><span class="id" title="definition">default_nan_pl32</span></a><br/> <span class="id" title="keyword">end</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="b32_opp"><span class="id" title="definition">b32_opp</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#Bopp"><span class="id" title="definition">Bopp</span></a> 24 128 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a>.<br/> <span class="id" title="keyword">Definition</span> <a name="b32_plus"><span class="id" title="definition">b32_plus</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#Bplus"><span class="id" title="definition">Bplus</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B32_Bits.Hprec"><span class="id" title="variable">Hprec</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B32_Bits.Hprec_emax"><span class="id" title="variable">Hprec_emax</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binop_nan_pl32"><span class="id" title="definition">binop_nan_pl32</span></a>.<br/> <span class="id" title="keyword">Definition</span> <a name="b32_minus"><span class="id" title="definition">b32_minus</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#Bminus"><span class="id" title="definition">Bminus</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B32_Bits.Hprec"><span class="id" title="variable">Hprec</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B32_Bits.Hprec_emax"><span class="id" title="variable">Hprec_emax</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binop_nan_pl32"><span class="id" title="definition">binop_nan_pl32</span></a>.<br/> <span class="id" title="keyword">Definition</span> <a name="b32_mult"><span class="id" title="definition">b32_mult</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#Bmult"><span class="id" title="definition">Bmult</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B32_Bits.Hprec"><span class="id" title="variable">Hprec</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B32_Bits.Hprec_emax"><span class="id" title="variable">Hprec_emax</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binop_nan_pl32"><span class="id" title="definition">binop_nan_pl32</span></a>.<br/> <span class="id" title="keyword">Definition</span> <a name="b32_div"><span class="id" title="definition">b32_div</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#Bdiv"><span class="id" title="definition">Bdiv</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B32_Bits.Hprec"><span class="id" title="variable">Hprec</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B32_Bits.Hprec_emax"><span class="id" title="variable">Hprec_emax</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binop_nan_pl32"><span class="id" title="definition">binop_nan_pl32</span></a>.<br/> <span class="id" title="keyword">Definition</span> <a name="b32_sqrt"><span class="id" title="definition">b32_sqrt</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#Bsqrt"><span class="id" title="definition">Bsqrt</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B32_Bits.Hprec"><span class="id" title="variable">Hprec</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B32_Bits.Hprec_emax"><span class="id" title="variable">Hprec_emax</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#unop_nan_pl32"><span class="id" title="definition">unop_nan_pl32</span></a>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="b32_of_bits"><span class="id" title="definition">b32_of_bits</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binary32"><span class="id" title="definition">binary32</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binary_float_of_bits"><span class="id" title="definition">binary_float_of_bits</span></a> 23 8 (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#refl_equal"><span class="id" title="abbreviation">refl_equal</span></a> <span class="id" title="var">_</span>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#refl_equal"><span class="id" title="abbreviation">refl_equal</span></a> <span class="id" title="var">_</span>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#refl_equal"><span class="id" title="abbreviation">refl_equal</span></a> <span class="id" title="var">_</span>).<br/> <span class="id" title="keyword">Definition</span> <a name="bits_of_b32"><span class="id" title="definition">bits_of_b32</span></a> : <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binary32"><span class="id" title="definition">binary32</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#bits_of_binary_float"><span class="id" title="definition">bits_of_binary_float</span></a> 23 8.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B32_Bits"><span class="id" title="section">B32_Bits</span></a>.<br/> <br/> </div> <div class="doc"> Specialization for IEEE double precision operations </div> <div class="code"> <span class="id" title="keyword">Section</span> <a name="B64_Bits"><span class="id" title="section">B64_Bits</span></a>.<br/> <br/> <span class="id" title="keyword">Implicit Arguments</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_nan"><span class="id" title="constructor">B754_nan</span></a> [[<span class="id" title="var">prec</span>] [<span class="id" title="var">emax</span>]].<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="binary64"><span class="id" title="definition">binary64</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#binary_float"><span class="id" title="inductive">binary_float</span></a> 53 1024.<br/> <br/> <span class="id" title="keyword">Let</span> <a name="B64_Bits.Hprec"><span class="id" title="variable">Hprec</span></a> : (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> 53)%<span class="id" title="var">Z</span>.<br/> <span class="id" title="keyword">Qed</span>.<br/> <br/> <span class="id" title="keyword">Let</span> <a name="B64_Bits.Hprec_emax"><span class="id" title="variable">Hprec_emax</span></a> : (53 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> 1024)%<span class="id" title="var">Z</span>.<br/> <span class="id" title="keyword">Qed</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="default_nan_pl64"><span class="id" title="definition">default_nan_pl64</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#nan_pl"><span class="id" title="definition">nan_pl</span></a> 53 :=<br/> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#exist"><span class="id" title="constructor">exist</span></a> <span class="id" title="var">_</span> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#iter_nat"><span class="id" title="definition">iter_nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xO"><span class="id" title="constructor">xO</span></a> 51 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xH"><span class="id" title="constructor">xH</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#refl_equal"><span class="id" title="abbreviation">refl_equal</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="unop_nan_pl64"><span class="id" title="definition">unop_nan_pl64</span></a> (<span class="id" title="var">f</span> : <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binary64"><span class="id" title="definition">binary64</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#nan_pl"><span class="id" title="definition">nan_pl</span></a> 53 :=<br/> <span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#f"><span class="id" title="variable">f</span></a> <span class="id" title="keyword">with</span><br/> | <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_nan"><span class="id" title="constructor">B754_nan</span></a> <span class="id" title="var">s</span> <span class="id" title="var">pl</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">s</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">pl</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/> | <span class="id" title="var">_</span> ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#default_nan_pl64"><span class="id" title="definition">default_nan_pl64</span></a><br/> <span class="id" title="keyword">end</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="binop_nan_pl64"><span class="id" title="definition">binop_nan_pl64</span></a> (<span class="id" title="var">pl1</span> <span class="id" title="var">pl2</span> : <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binary64"><span class="id" title="definition">binary64</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#nan_pl"><span class="id" title="definition">nan_pl</span></a> 53 :=<br/> <span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#pl1"><span class="id" title="variable">pl1</span></a>, <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#pl2"><span class="id" title="variable">pl2</span></a> <span class="id" title="keyword">with</span><br/> | <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_nan"><span class="id" title="constructor">B754_nan</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">pl1</span>, <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">s1</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#pl1"><span class="id" title="variable">pl1</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/> | <span class="id" title="var">_</span>, <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#B754_nan"><span class="id" title="constructor">B754_nan</span></a> <span class="id" title="var">s2</span> <span class="id" title="var">pl2</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">s2</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#pl2"><span class="id" title="variable">pl2</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/> | <span class="id" title="var">_</span>, <span class="id" title="var">_</span> ⇒ <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#default_nan_pl64"><span class="id" title="definition">default_nan_pl64</span></a><br/> <span class="id" title="keyword">end</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="b64_opp"><span class="id" title="definition">b64_opp</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#Bopp"><span class="id" title="definition">Bopp</span></a> 53 1024 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a>.<br/> <span class="id" title="keyword">Definition</span> <a name="b64_plus"><span class="id" title="definition">b64_plus</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#Bplus"><span class="id" title="definition">Bplus</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B64_Bits.Hprec"><span class="id" title="variable">Hprec</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B64_Bits.Hprec_emax"><span class="id" title="variable">Hprec_emax</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binop_nan_pl64"><span class="id" title="definition">binop_nan_pl64</span></a>.<br/> <span class="id" title="keyword">Definition</span> <a name="b64_minus"><span class="id" title="definition">b64_minus</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#Bminus"><span class="id" title="definition">Bminus</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B64_Bits.Hprec"><span class="id" title="variable">Hprec</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B64_Bits.Hprec_emax"><span class="id" title="variable">Hprec_emax</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binop_nan_pl64"><span class="id" title="definition">binop_nan_pl64</span></a>.<br/> <span class="id" title="keyword">Definition</span> <a name="b64_mult"><span class="id" title="definition">b64_mult</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#Bmult"><span class="id" title="definition">Bmult</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B64_Bits.Hprec"><span class="id" title="variable">Hprec</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B64_Bits.Hprec_emax"><span class="id" title="variable">Hprec_emax</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binop_nan_pl64"><span class="id" title="definition">binop_nan_pl64</span></a>.<br/> <span class="id" title="keyword">Definition</span> <a name="b64_div"><span class="id" title="definition">b64_div</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#Bdiv"><span class="id" title="definition">Bdiv</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B64_Bits.Hprec"><span class="id" title="variable">Hprec</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B64_Bits.Hprec_emax"><span class="id" title="variable">Hprec_emax</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binop_nan_pl64"><span class="id" title="definition">binop_nan_pl64</span></a>.<br/> <span class="id" title="keyword">Definition</span> <a name="b64_sqrt"><span class="id" title="definition">b64_sqrt</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE.html#Bsqrt"><span class="id" title="definition">Bsqrt</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B64_Bits.Hprec"><span class="id" title="variable">Hprec</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B64_Bits.Hprec_emax"><span class="id" title="variable">Hprec_emax</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#unop_nan_pl64"><span class="id" title="definition">unop_nan_pl64</span></a>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="b64_of_bits"><span class="id" title="definition">b64_of_bits</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binary64"><span class="id" title="definition">binary64</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binary_float_of_bits"><span class="id" title="definition">binary_float_of_bits</span></a> 52 11 (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#refl_equal"><span class="id" title="abbreviation">refl_equal</span></a> <span class="id" title="var">_</span>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#refl_equal"><span class="id" title="abbreviation">refl_equal</span></a> <span class="id" title="var">_</span>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#refl_equal"><span class="id" title="abbreviation">refl_equal</span></a> <span class="id" title="var">_</span>).<br/> <span class="id" title="keyword">Definition</span> <a name="bits_of_b64"><span class="id" title="definition">bits_of_b64</span></a> : <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#binary64"><span class="id" title="definition">binary64</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> := <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#bits_of_binary_float"><span class="id" title="definition">bits_of_binary_float</span></a> 52 11.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Appli.Fappli_IEEE_bits.html#B64_Bits"><span class="id" title="section">B64_Bits</span></a>.<br/> </div> </div> <div id="footer"> <hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> </div> </div> </body> </html>
distrib
>
Mageia
>
6
>
armv5tl
>
media
>
core-release
>
by-pkgid
>
3c7997fe0e8405f6d7b5563e63d17a78
>
files
>
73
