bigenough

The package contains a package to reasoning with big enough objects (mostly natural numbers). This package is essentially for backward compatibility purposes as bigenough will be subsumed by the near tactics. The formalization is based on the Mathematical Components library.

Meta

• Author(s):
  • Cyril Cohen
• License: CeCILL-B
• Compatible Coq versions: 8.10 or later
• Additional dependencies:
  • MathComp ssreflect 1.6 or later
• Coq namespace: mathcomp.bigenough
• Related publication(s): none

Building and installation instructions

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

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-bigenough

To instead build and install manually, do:

git clone https://github.com/math-comp/bigenough.git
cd bigenough
make   # or make -j <number-of-cores-on-your-machine> 
make install

A small library to do epsilon - N reasoning.

This repository is essentially for archiving purposes as bigenough will be subsumed by the near tactics.

The formalization is based on the Mathematical Components library for the Coq proof assistant, although it requires only the ssreflect package.