Library Stdlib.Floats.Floats
The Floats library is split in 6 theories:
For a brief overview of the Floats library,
see https://coq.inria.fr/distrib/current/refman/language/coq-library.html#floats-library
N.B.: This library only offers a bit-level specification of floating-point
arithmetic. For a more complete set of theorems, including links with real
arithmetic, see the Flocq library https://flocq.gitlabpages.inria.fr/
- FloatClass: define the float_class inductive
- PrimFloat: define the floating-point values and operators as kernel primitives
- SpecFloat: specify the floating-point operators with binary integers
- FloatOps: define conversion functions between spec_float and float
- FloatAxioms: state properties of the primitive operators w.r.t. spec_float
- FloatLemmas: prove a few results involving Z.frexp and Z.ldexp
From Stdlib Require Export FloatClass.
From Stdlib Require Export PrimFloat.
From Stdlib Require Export SpecFloat.
From Stdlib Require Export FloatOps.
From Stdlib Require Export FloatAxioms.
From Stdlib Require Export FloatLemmas.