Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
F
flocq
Project overview
Project overview
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
1
Issues
1
List
Boards
Labels
Milestones
Merge Requests
1
Merge Requests
1
Packages
Packages
Container Registry
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Commits
Issue Boards
Open sidebar
Flocq
flocq
Commits
ec58e33a
Commit
ec58e33a
authored
Oct 01, 2010
by
Guillaume Melquiond
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Added license banner to the .v files.
parent
b574e6b5
Changes
25
Hide whitespace changes
Inline
Sidebyside
Showing
25 changed files
with
450 additions
and
0 deletions
+450
0
src/Appli/Fappli_Axpy.v
src/Appli/Fappli_Axpy.v
+18
0
src/Calc/Fcalc_bracket.v
src/Calc/Fcalc_bracket.v
+18
0
src/Calc/Fcalc_digits.v
src/Calc/Fcalc_digits.v
+18
0
src/Calc/Fcalc_div.v
src/Calc/Fcalc_div.v
+18
0
src/Calc/Fcalc_ops.v
src/Calc/Fcalc_ops.v
+18
0
src/Calc/Fcalc_round.v
src/Calc/Fcalc_round.v
+18
0
src/Calc/Fcalc_round_FIX.v
src/Calc/Fcalc_round_FIX.v
+18
0
src/Calc/Fcalc_sqrt.v
src/Calc/Fcalc_sqrt.v
+18
0
src/Core/Fcore.v
src/Core/Fcore.v
+18
0
src/Core/Fcore_FIX.v
src/Core/Fcore_FIX.v
+18
0
src/Core/Fcore_FLT.v
src/Core/Fcore_FLT.v
+18
0
src/Core/Fcore_FLX.v
src/Core/Fcore_FLX.v
+18
0
src/Core/Fcore_FTZ.v
src/Core/Fcore_FTZ.v
+18
0
src/Core/Fcore_Raux.v
src/Core/Fcore_Raux.v
+18
0
src/Core/Fcore_defs.v
src/Core/Fcore_defs.v
+18
0
src/Core/Fcore_float_prop.v
src/Core/Fcore_float_prop.v
+18
0
src/Core/Fcore_generic_fmt.v
src/Core/Fcore_generic_fmt.v
+18
0
src/Core/Fcore_rnd.v
src/Core/Fcore_rnd.v
+18
0
src/Core/Fcore_rnd_ne.v
src/Core/Fcore_rnd_ne.v
+18
0
src/Core/Fcore_ulp.v
src/Core/Fcore_ulp.v
+18
0
src/Prop/Fprop_Sterbenz.v
src/Prop/Fprop_Sterbenz.v
+18
0
src/Prop/Fprop_div_sqrt_error.v
src/Prop/Fprop_div_sqrt_error.v
+18
0
src/Prop/Fprop_mult_error.v
src/Prop/Fprop_mult_error.v
+18
0
src/Prop/Fprop_plus_error.v
src/Prop/Fprop_plus_error.v
+18
0
src/Prop/Fprop_relative.v
src/Prop/Fprop_relative.v
+18
0
No files found.
src/Appli/Fappli_Axpy.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore
.
Section
Axpy
.
...
...
src/Calc/Fcalc_bracket.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore
.
Section
Fcalc_bracket
.
...
...
src/Calc/Fcalc_digits.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore
.
Section
Fcalc_digits
.
...
...
src/Calc/Fcalc_div.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore
.
Require
Import
Fcalc_bracket
.
Require
Import
Fcalc_digits
.
...
...
src/Calc/Fcalc_ops.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore_Raux
.
Require
Import
Fcore_defs
.
Require
Import
Fcore_float_prop
.
...
...
src/Calc/Fcalc_round.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore
.
Require
Import
Fcalc_bracket
.
Require
Import
Fcalc_digits
.
...
...
src/Calc/Fcalc_round_FIX.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore
.
Require
Import
Fcalc_bracket
.
Require
Import
Fcalc_digits
.
...
...
src/Calc/Fcalc_sqrt.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore
.
Require
Import
Fcalc_bracket
.
Require
Import
Fcalc_digits
.
...
...
src/Core/Fcore.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Export
Fcore_Raux
.
Require
Export
Fcore_defs
.
Require
Export
Fcore_float_prop
.
...
...
src/Core/Fcore_FIX.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore_Raux
.
Require
Import
Fcore_defs
.
Require
Import
Fcore_rnd
.
...
...
src/Core/Fcore_FLT.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore_Raux
.
Require
Import
Fcore_defs
.
Require
Import
Fcore_rnd
.
...
...
src/Core/Fcore_FLX.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore_Raux
.
Require
Import
Fcore_defs
.
Require
Import
Fcore_rnd
.
...
...
src/Core/Fcore_FTZ.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore_Raux
.
Require
Import
Fcore_defs
.
Require
Import
Fcore_rnd
.
...
...
src/Core/Fcore_Raux.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Export
Reals
.
Require
Export
ZArith
.
...
...
src/Core/Fcore_defs.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore_Raux
.
Section
Def
.
...
...
src/Core/Fcore_float_prop.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore_Raux
.
Require
Import
Fcore_defs
.
...
...
src/Core/Fcore_generic_fmt.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore_Raux
.
Require
Import
Fcore_defs
.
Require
Import
Fcore_rnd
.
...
...
src/Core/Fcore_rnd.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore_Raux
.
Require
Import
Fcore_defs
.
...
...
src/Core/Fcore_rnd_ne.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore_Raux
.
Require
Import
Fcore_defs
.
Require
Import
Fcore_rnd
.
...
...
src/Core/Fcore_ulp.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore_Raux
.
Require
Import
Fcore_defs
.
Require
Import
Fcore_rnd
.
...
...
src/Prop/Fprop_Sterbenz.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore
.
Require
Import
Fcalc_ops
.
...
...
src/Prop/Fprop_div_sqrt_error.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore
.
Require
Import
Fcalc_ops
.
Require
Import
Fprop_relative
.
...
...
src/Prop/Fprop_mult_error.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore
.
Require
Import
Fcalc_ops
.
...
...
src/Prop/Fprop_plus_error.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore
.
Require
Import
Fcalc_ops
.
...
...
src/Prop/Fprop_relative.v
View file @
ec58e33a
(
*
This
file
is
part
of
the
Flocq
formalization
of
floating

point
arithmetic
in
Coq
:
http
:
//flocq.gforge.inria.fr/
Copyright
(
C
)
2010
Sylvie
Boldo
Copyright
(
C
)
2010
Guillaume
Melquiond
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
.
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
.
*
)
Require
Import
Fcore
.
Section
Fprop_relative
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment