Coq and its Platform
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.17.1 along with CoqIDE and number of Coq plugins and libraries. Please refer to
https://github.com/coq/platform/blob/main/doc/README%7E8.17%7E2023.08.md
for the complete list of packages and additional information like licenses.