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
This snap contains the Coq prover version 8.17.1 along with CoqIDE and number of Coq plugins and libraries. Please refer to
For versions of Ubuntu between 14.04 LTS (Trusty Tahr) and 15.10 (Wily Werewolf), as well as Ubuntu flavours that don’t include snap by default, snap can be installed from the Ubuntu Software Centre by searching for snapd.
Alternatively, snapd can be installed from the command line:
sudo apt update
sudo apt install snapd
Either log out and back in again, or restart your system, to ensure snap’s paths are updated correctly.
Install Coq Interactive Theorem Prover
To install Coq Interactive Theorem Prover, simply use the following command: