Package 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.

Typical applications include the certification of properties of
programming languages (e.g. the CompCert compiler certification project,
or the Bedrock verified low-level programming library), the formalization
of mathematics (e.g. the full formalization of the Feit-Thompson theorem
or homotopy type theory) and teaching.

Version: 8.13.2

See also: coq-coqide.

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 and Caml programs
coqdoc A documentation tool for the Coq proof assistant
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