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

Ltac2

• A Brief Introduction to ML like languages
• A brief introduction to manipulating tactics and thunking in Ltac2 interactive version and source code
• Introduction to Ltac2
• Quoting in Ltac2
• Matching Terms and Goals in Ltac2
• Backtracking in Ltac2 interactive version and source code
• Notations in Ltac2

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