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
The packages for RHEL 8 and RHEL 7 are in each distribution’s respective Extra Packages for Enterprise Linux (EPEL) repository. The instructions for adding this repository diverge slightly between RHEL 8 and RHEL 7, which is why they’re listed separately below.
The EPEL repository can be added to RHEL 8 with the following command: