1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
Source: coq-float
Section: math
Priority: optional
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Uploaders:
Samuel Mimram <smimram@debian.org>,
Stéphane Glondu <glondu@debian.org>
Build-Depends: debhelper (>= 9), coq (>= 8.4)
Standards-Version: 3.9.5
Homepage: http://lipforge.ens-lyon.fr/www/pff/
Vcs-Browser: http://anonscm.debian.org/gitweb/?p=pkg-ocaml-maint/packages/coq-float.git
Vcs-Git: git://anonscm.debian.org/pkg-ocaml-maint/packages/coq-float.git
Package: libfloat-coq
Architecture: all
Depends: ${shlibs:Depends}, ${misc:Depends}, coq-${F:CoqABI}
Description: Coq library on floating-point arithmetic
This package provides PFF (Preuves Formelles sur les Flottants =
Formal Proofs about Floats), a library for reasoning about
floating-point arithmetic in Coq. It contains both definitions and
proofs of basic facts, old & new properties and algorithms.
|
