First Steps
A Tour of Rocq
Rocq Platform Docs
About
Programming
Equations Plugin
Structures
Hierarchy Builder Plugin
Metaprogramming
Ltac2
Writing Proofs
Tutorials
- 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
Help Improve Our Documentation
All Rocq docs are open source. See something that's wrong or unclear? Submit a pull request.
On This Page