Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library
Clone or download
herbelin Merge pull request #12 from herbelin/master+compat-pr7762-bind-multip…
…le-scope

Avoid binding several types at once to the same scope, preparing Coq to PR #7762
Latest commit f1a63cb Sep 24, 2018

README.md

The BigNums Library

Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library.

TODO

  • Documentation
  • Add a Makefile in the tests/ directory

Authors

Copyright INRIA 2007-2017.

Initial Code by Laurent Théry, Benjamin Grégoire, Arnaud Spiwack. Many revisions by Evgeny Makarov and Pierre Letouzey.

License

LGPL 2.1