Summary
Flocq (Floats for Coq) is a formalization of floating-point arithmetic for the Coq proof assistant. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.
Versions
v4.1.1 :: 0 :: gentoo
- Modified
- License
- LGPL-3
- Keywords
- ~amd64 ~x86
v4.1.0-r1 :: 0 :: gentoo
- Modified
- License
- LGPL-3
- Keywords
- ~amd64 ~x86
Dependencies
dev-lang / ocaml : Programming language supporting functional, imperative & object-oriented styles
sci-mathematics / coq : Proof assistant written in O'Caml
Runtime Dependencies
dev-lang / ocaml : Programming language supporting functional, imperative & object-oriented styles
sci-mathematics / coq : Proof assistant written in O'Caml
Depending packages
sci-mathematics / gappalib-coq : Allows the certificates Gappa generates to be imported by the Coq
Bugs
Change logs
- Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/flocq: ignore CFLAGS for ML/Coq code
Closes: https://bugs.gentoo.org/904156 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/flocq: bump to 4.1.1
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/flocq: fix deps
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/flocq: new package; add 4.1.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org>