Welcome to the Coq Discourse forum! This forum is for anyone wanting to ask questions or discuss any topic related to the use or the development of the Coq proof assistant, and related type-theoretic foundations.
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Go to https://coq.inria.fr to learn more.
You may use this forum to:
- ask questions and learn about how to use Coq or the underlying type theoretic foundations;
- discuss how to organize a Coq library, develop a plugin, or participate in the development of Coq;
- announce events (related conferences and workshops, Coq meetups, etc.), package releases, call for papers, etc.;
- discuss any related topic, blog posts, etc.
The default language for the forum is English, however you are welcome to use other languages if you prefer. There are languages for which a special category is dedicated. If you create a new post in one of these languages, the norm is to use the corresponding category.
The following wiki page contains some useful information on Discourse, in particular some advice on how to use Discourse via e-mail: https://github.com/coq/coq/wiki/Discourse