First Steps
A Tour of Rocq
Rocq Platform Docs
About
Programming
Equations Plugin
Structures
Hierarchy Builder Plugin
Metaprogramming
Ltac2
Theory of Rocq
Explanations
- Template Polymorphism vs. Universe Polymorphism: interactive version and source code
- Explanation of bidirectionality hints: 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