Fedora Packages

rocq-core Subpackage of rocq

The Rocq Prelude, and the Corelib and Ltac2 modules

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 includes the Rocq prelude, that is loaded automatically by Rocq in every .v file, as well as other modules bound to the Corelib.* and Ltac2.* namespaces.

Releases Overview

Release Stable Testing
Fedora Rawhide 9.1.1-1.fc45 -
Fedora 44 - 9.1.1-1.fc44
File a new bug report »
Package Info
  • Upstream: https://rocq-prover.org/
  • License(s): LGPL-2.1-only AND LGPL-2.1-only WITH OCaml-LGPL-linking-exception AND MIT AND BSD-3-Clause
  • Maintainer: jjames
Related Packages

You can contact the maintainers of this package via email at rocq dash maintainers at fedoraproject dot org.


Sources on Pagure