Awesome
<!--- This file was generated from `meta.yml`, please do not edit manually. Follow the instructions on https://github.com/coq-community/templates to regenerate. --->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.