Your company here, and a link to your site. Click to find out more.

Package coq-core

Core components of the coq proof management system


Coq is a formal proof management system. It 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 package includes the Coq core binaries, plugins, and tools, but not
the vernacular standard library.

Version: 8.18.0

General Commands

coq-tex Process Coq phrases embedded in LaTeX files
coq_makefile The Coq Proof Assistant makefile generator
coqc The Coq Proof Assistant compiler
coqchk The Coq Proof Checker compiled libraries verifier
coqdep Compute inter-module dependencies for Coq programs
coqdoc A documentation tool for the Coq proof assistant
coqnative The Coq native compiler
coqtop The Coq Proof Assistant toplevel system
coqtop.byte The bytecode Coq toplevel
coqtop.opt The native-code Coq toplevel
coqwc print the number of specification, proof and comment lines in Coq files