Coq Interactive Theorem Prover

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)