rocqideversion Documentation on ocaml.org

The Rocq Prover --- GTK3 IDE

The Rocq Prover is an interactive theorem prover, or proof assistant. 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 the RocqIDE, a graphical user interface for the development of interactive proofs.

AuthorThe Rocq development team, INRIA, CNRS, and contributors
LicenseLGPL-2.1-only
Published
Homepagehttps://rocq-prover.org/
Issue Trackerhttps://github.com/rocq-prover/rocq/issues
MaintainerThe Rocq development team <rocq+rocq-development@discoursemail.com>
Dependencies
Source [http] https://github.com/rocq-prover/rocq/releases/download/V9.2.0/rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/rocqide/rocqide.9.2.0/opam
No package is dependent