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 |