Coq Platform Docs - Demo

View Coq-Platform-Doc

About

This is a demo page for the Coq Platform Docs. These tutorials are meant to become part of Rocq's next website and the github repository should be part of the Coq organization.

The interactive versions can be run in a web browser, for the source code, one needs a text editor able to interact with Coq (e.g. CoqIDE, emacs with Proof General, vim with CoqTail, vscode with vscoq).

Coq Tutorials

• Search Tutorial: interactive version and source code
• Basic library files and module management: interactive version and source code
• Explanation of template vs. “full” universe polymorphism: interactive version and source code

Equations tutorials

• Basics: interactive version and source code
• Obligations: interactive version and source code
• Well-founded recursion: interactive version and source code