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.20.1
General Commands | |
| coq-tex | process Coq phrases embedded in LaTeX files |
| coq_makefile | generate makefiles for Coq proof development |
| coqc | Coq compiler |
| coqchk | verify compiled Coq libraries |
| coqdep | compute inter-module dependencies for Coq programs |
| coqdoc | documentation tool for the Coq proof assistant |
| coqnative | native Coq compiler |
| coqtop | toplevel Coq system |
| coqtop.byte | bytecode toplevel Coq system |
| coqwc | print the number of specification, proof and comment lines in Coq files |