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
This package provides CoqIDE, a graphical user interface for the
development of interactive proofs.
See also: coq.
|coqide||The Coq Proof Assistant graphical interface|