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 |