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:


Get it from the Snap Store

Search for another snap, or go back to the homepage.