Language

Package: coq-flocq @ 4.1.0

Synopsis

Floating-point formalization for the Coq system

Description

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.

Home page
https://flocq.gitlabpages.inria.fr
Location
gnu/packages/coq.scm (line: 243, column: 2)
License

Derivations

SystemTargetDerivationBuild status
x86_64-linux/gnu/store/46rk0i6zkij8f49lhai2mdcgf452brw7-coq-flocq-4.1.0.drv
x86_64-linuxx86_64-w64-mingw32/gnu/store/scc7im8zwyhylpyjsyh5l605mxq6rfd5-coq-flocq-4.1.0.drv
x86_64-linuxriscv64-linux-gnu/gnu/store/k97zvsrsx9xp7psg077h4q4ziq0h14w8-coq-flocq-4.1.0.drv
x86_64-linuxpowerpc-linux-gnu/gnu/store/sva0jq4ikq963c4c91rc170npxapnq6s-coq-flocq-4.1.0.drv
x86_64-linuxpowerpc64le-linux-gnu/gnu/store/fg8d2wby7c78h35hvgwimd0xk5gy82wk-coq-flocq-4.1.0.drv
x86_64-linuxmips64el-linux-gnu/gnu/store/izsjjygrhksrphrspg13cgb8gdai68bp-coq-flocq-4.1.0.drv
x86_64-linuxi686-w64-mingw32/gnu/store/lvv83h1jvsxirq76qvcf64b2s9hiklbb-coq-flocq-4.1.0.drv
x86_64-linuxi586-pc-gnu/gnu/store/xp9dqil4v52i7gvrn8ri4bqfmqfm9l6r-coq-flocq-4.1.0.drv
x86_64-linuxarm-linux-gnueabihf/gnu/store/wmhyj1bawn6w2nphmv2xn655qicxfaqq-coq-flocq-4.1.0.drv
x86_64-linuxaarch64-linux-gnu/gnu/store/sqkkwsmkkgdkw96jixqnw06yz9ki02w8-coq-flocq-4.1.0.drv
riscv64-linux/gnu/store/b839l3dhw1q0lkf5ykv67iyp003879gk-coq-flocq-4.1.0.drv
    powerpc-linux/gnu/store/9qzi7477x9x00g1w4x4fhlhx9jv828sn-coq-flocq-4.1.0.drv
      powerpc64le-linux/gnu/store/iwwc7fsdd9s749h825snz81h6daia6ai-coq-flocq-4.1.0.drv
      mips64el-linux/gnu/store/c7lcmc24bi2jlp5rs54d090c1y2218gm-coq-flocq-4.1.0.drv
        i686-linux/gnu/store/924isdb5li2r761wh3d92qmbrb8aybpc-coq-flocq-4.1.0.drv
        i586-gnu/gnu/store/x54f8wb7vm6r8rv9sdh7wd84p9n971rd-coq-flocq-4.1.0.drv
        armhf-linux/gnu/store/d0ywca3q75a8d97xi17mb651czxdcy31-coq-flocq-4.1.0.drv
        aarch64-linux/gnu/store/xady48np03sbkylvp261jv06mhi7v8g4-coq-flocq-4.1.0.drv

        Lint warnings

        LinterMessageLocation
        optional-tests

        Make sure tests are only run when requested

        the 'check' phase should respect #:tests?
        optional-tests

        Make sure tests are only run when requested

        the 'check' phase should respect #:tests?