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.15.1 along with CoqIDE and number of Coq plugins and libraries. Please refer to

for the complete list of packages and additional information like licenses.


Get it from the Snap Store

Search for another snap, or go back to the homepage.
An error has occurred. This application may no longer respond until reloaded. Reload 🗙