⚠️ Under construction ⚠️ This website will be officialy launched with the first release of Rocq 9.0 in March 2025. Until then, there may remain broken links and references to not-yet existing projects.

First Steps

Documentation

The Rocq Platform Docs Documentation of Rocq Documentation of Equations

Documentation of Rocq

Writing Proofs

Introducing Hypothesis with Intro Patterns to Factorize proofs interactive version and source code
Chaining Tactics to Simplify and Factorize proofs interactive version and source code

Rocq Features

Searching for Definitions and Lemma interactive version and source code
Basic Library Files and Module Management interactive version and source code

Rocq's Theory

Template Polymorphism vs. Universe Polymorphism: interactive version and source code
Explanation of bidirectionality hints: interactive version and source code

Still need help?

Ask the Rocq Community

Search the Rocq Wiki

Help Improve Our Documentation

All Rocq docs are open source. See something that's wrong or unclear? Submit a pull request.

On This Page

Writing Proofs
Rocq Features
Rocq's Theory