Bignums

This Coq library provides BigN, BigZ, and BigQ that used to be part of the standard library.

Meta

• Author(s):
  • Laurent Théry
  • Benjamin Grégoire
  • Arnaud Spiwack
  • Evgeny Makarov
  • Pierre Letouzey
• Rocq-community maintainer(s):
  • Pierre Roux (@proux01)
  • Érik Martin-Dorel (@erikmd)
• License: GNU Lesser General Public License v2.1
• Compatible Rocq/Coq versions: master (use the corresponding branch or release for other Coq versions)
• Compatible OCaml versions: all versions supported by Coq
• Additional dependencies: none
• Rocq/Coq namespace: Bignums
• Related publication(s): none

Building and installation instructions

The easiest way to install the latest released version of Bignums is via OPAM:

opam repo add rocq-released https://rocq-prover.org/opam/released
opam install coq-bignums

To instead build and install manually, do:

git clone https://github.com/coq-community/bignums.git
cd bignums
make   # or make -j <number-of-cores-on-your-machine> 
make install