rocq-doc Subpackage of rocq

Rocq 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 provides documentation and tutorials for the system. The main documentation comes in two parts: the main Library documentation, which describes all Corelib.* modules, and the Reference Manual, which gives a more complete description of the whole system. Included are HTML versions of both and a PDF version of the Reference Manual.

Releases Overview