Coq and its Platform
The Coq interactive prover provides a formal language to write
mathematical definitions, executable algorithms, and theorems, together
with an environment for semi-interactive development of machine-checked
proofs.
This snap contains the Coq prover version 8.13.2
along with CoqIDE and the following packages:
- aac-tactics: Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators (version: 8.13.0, license: LGPL-3.0-or-later)
- bignums: Bignums, the Coq library of arbitrary large numbers (version: 8.13.0, license: LGPL-2.1-only)
- compcert: The CompCert C compiler (64 bit) (version: 3.8, license: INRIA Non-Commercial License Agreement)
- coquelicot: A Coq formalization of real analysis compatible with the standard library (version: 3.1.0, license: LGPL-3.0-or-later)
- elpi: Elpi extension language for Coq (version: 1.8.1, license: LGPL-2.1-or-later)
- equations: A function definition package for Coq (version: 1.2.3+8.13, license: LGPL-2.1-or-later)
- ext-lib: A library of Coq definitions, theorems, and tactics (version: 0.11.3, license: BSD-2-Clause-FreeBSD)
- flocq: A formalization of floating-point arithmetic for the Coq system (version: 3.3.1, license: LGPL-3.0-or-later)
- gappa: A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover (version: 1.4.6, license: LGPL-3.0-or-later)
- hierarchy-builder: High level commands to declare and evolve a hierarchy based on packed classes (version: 1.0.0, license: MIT)
- hott: The Homotopy Type Theory library (version: 8.13, license: BSD-2-Clause)
- interval: A Coq tactic for proving bounds on real-valued expressions automatically (version: 4.1.1, license: CeCILL-C)
- mathcomp-algebra: Mathematical Components Library on Algebra (version: 1.12.0, license: CECILL-B)
- mathcomp-bigenough: A small library to do epsilon - N reasonning (version: 1.0.0, license: CeCILL-B)
- mathcomp-character: Mathematical Components Library on character theory (version: 1.12.0, license: CECILL-B)
- mathcomp-field: Mathematical Components Library on Fields (version: 1.12.0, license: CECILL-B)
- mathcomp-fingroup: Mathematical Components Library on finite groups (version: 1.12.0, license: CECILL-B)
- mathcomp-finmap: Finite sets, finite maps, finitely supported functions (version: 1.5.1, license: CECILL-B)
- mathcomp-real-closed: Mathematical Components Library on real closed fields (version: 1.1.2, license: CECILL-B)
- mathcomp-solvable: Mathematical Components Library on finite groups (II) (version: 1.12.0, license: CECILL-B)
- mathcomp-ssreflect: Small Scale Reflection (version: 1.12.0, license: CECILL-B)
- menhirlib: A support library for verified Coq parsers produced by Menhir (version: 20200624, license: LGPL-3.0-or-later)
- mtac2: Mtac2: Typed Tactics for Coq (version: 1.4+8.13, license: MIT)
- quickchick: Randomized Property-Based Testing Plugin for Coq (version: 1.5.0, license: MIT)
- simple-io: IO monad for Coq (version: 1.5.0, license: MIT)
- unicoq: An enhanced unification algorithm for Coq (version: 1.5+8.13, license: MIT)
- vst: Verified Software Toolchain (version: 2.7.1, license: https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE)
Developer website
Contact Coq Development Team