Overview

Formalization of floating point numbers for Coq

Edit Package flocq

Flocq (Floats for Coq) is a floating-point formalization for the Coq
system. It provides a comprehensive library of theorems on a
multi-radix multi-precision arithmetic. It also supports efficient
numerical computations inside Coq.

  • Developed at science
  • Sources inherited from project openSUSE:Factory
  • 1 derived packages
  • Download package
  • osc -A https://api.opensuse.org checkout home:adrianSuSE:PL/flocq && cd $_
  • Create Badge
Refresh
Source Files
Filename Size Changed
flocq-4.2.2.tar.gz 0000448013 438 KB
flocq-rpmlintrc 0000000255 255 Bytes
flocq.changes 0000004215 4.12 KB
flocq.spec 0000005292 5.17 KB
Comments 1
Factory Maintainer's avatar
Factory Maintainer (factory-maintainer) -

<!-- Installcheck -->

Installcheck problems for x86_64

  • nothing provides ocaml(NStdlib_Arith_Factorial) = a4d85fcd88df76861d18b98ac16b0b14 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Arith_PeanoNat) = 8bf1695592ca75ace35a19a35ba33063 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Bool_Bool) = 985c858c7c0619de4a3121592aee4ee7 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Classes_DecidableClass) = 63d9ba73dcbd7f38864f72ce7d71b716 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Logic_HLevelsBase) = 405f403e0e769625cc3f36a07ba87243 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_NArith_BinNat) = 55292bbd81b1aa2a57ed363ca0e48722 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_PArith_BinPos) = fe27dd62f1827512c5aed7cfd48a5e49 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_QArith_QArith_base) = f39c02c6251e7243da7f09ee500d6f34 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_QArith_Qabs) = c38781add29938f16f4a5f037074257a needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_QArith_Qreduction) = c67ad6228b1def00b89d6d87e7318162 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_Alembert) = 437687c70950ec408c6b1234472a9cbe needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_Cauchy_ConstructiveCauchyReals) = 6b1b0c42abd01d2e2154231c77d756a8 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_Cauchy_ConstructiveCauchyRealsMult) = 9978f54ef63101a7b0401022433d1059 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_Cauchy_QExtra) = 6d96ce9907c27bfaf358ff1664773587 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_RIneq) = 7c003b8511279c5785ccc9a99b9e093a needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_R_sqrt) = 4b8977f71a169b7fadb7775d8eca5290 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_Raxioms) = 05505a8ee46e3f6e3beb67a33ea6e3a0 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_Rbasic_fun) = f14286846678cb5295f5166be35b3141 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_Rdefinitions) = ac84be43c7fc48da9c781abecf8bd03a needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_Rfunctions) = 0022e1a401776aa4a022f9da95e6cb74 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_Rpow_def) = 1ad5cef5e7b17ea161786be5d6ef2231 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_Rpower) = d4e4b20063e5d6ea27676ffa4cafb27e needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_Rsqrt_def) = 509e823d50277ab4e9f35cd927b9748a needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_Rtrigo_def) = 0cfe03dcd0700f92fdc73cfdf7029b92 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Reals_Rtrigo_fun) = ceb81df9d7fdc65d356cc619925a5305 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_Structures_OrdersTac) = a696b652182ce3a2ed0e037ccd0c81aa needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_ZArith_BinInt) = 9872cc943a4a49dd53ff0d9a7b4f583a needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_ZArith_ZArith_dec) = f64c8786ca7ac20f15fde1016239a619 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_ZArith_Zpower) = 17fb5db57ffecb2cc789574d7086746b needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocaml(NStdlib_setoid_ring_Ring_theory) = 5fece910fcd45c6606426c3d9aea011a needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocamlx(NStdlib_Bool_Bool) = 7d1d70f5677d0ca5be2a228e8f55b974 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocamlx(NStdlib_NArith_BinNat) = 37fa1a194577763c62641308b7fccd4d needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocamlx(NStdlib_PArith_BinPos) = 7b75417003bf85b229f9abd0f864591b needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocamlx(NStdlib_Reals_RIneq) = 857919b8cdcd09b431d5fccb9486a91c needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocamlx(NStdlib_Reals_R_sqrt) = 769b41673072f81a69333d8b922c4cb8 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocamlx(NStdlib_Reals_Rbasic_fun) = 481a7b6fcce036b459f7054b99e5be52 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocamlx(NStdlib_Reals_Rdefinitions) = 8b67ebb37e42834532d9b1987c16c328 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocamlx(NStdlib_Reals_Rfunctions) = d9456cd0f245ad27dc7255f49bcc06db needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocamlx(NStdlib_Reals_Rpower) = 311d0dfc0800b573c28dac15352f464e needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocamlx(NStdlib_ZArith_BinInt) = 16b433a021541312e08f2adb1c583f77 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocamlx(NStdlib_ZArith_ZArith_dec) = a09e4ce9e8ac1946214727cc9b0cfe47 needed by flocq-devel-4.2.2.x86_64
  • nothing provides ocamlx(NStdlib_ZArith_Zpower) = 1bee3a41a8ee2b64b88fa10b0c2252ce needed by flocq-devel-4.2.2.x86_64
openSUSE Build Service is sponsored by
Places