Coq

Join the Coq Track
TODO: The maintainers have not provided a description for this track.
Join the Coq Track
Track mentors

0 Mentors

Our mentors are friendly, experienced Coq developers who will help teach you new techniques and tricks.
Track students

16 Students

Join hundreds of students who have enjoyed learning and improving their skills by taking this track.
Track exercises

3 Exercises

Hundreds of hours have gone into making these exercises fun, useful, and challenging to help you enjoy learning.

About Coq

Require Import Coq.Strings.String.

Open Scope string_scope.

Definition hello:string := "Hello, World!".

(* Unit test *)
Lemma HelloTest:
  hello = "Hello, World!" .
Proof.
  reflexivity.
Qed.
Join the Coq track

A tremendous learning opportunity to explore the depth of your own knowledge

Exercism is fantastic in learning new languages but that is not the extent of it. If you are a "more experienced" programmer you may have encountered impostor syndrome: the idea you don't really know what you think you know. Exercism lets you solve problems and put them in the space of open feedback which is a tremendous learning opportunity to explore the depth of your own knowledge. Even if you have been programming in a language for awhile it is worth checking into Exercism to see where you stand with current implementation practices.

Fun. Challenging. Interesting

Community-sourced Coq exercises

These are a few of the 3 exercises on the Coq track. You can see all the exercises here.

Hello World
easy
misc
RNA Transcription
easy
misc
Tautology
easy
misc

Get started with the Coq track. As with everything on Exercism, it's 100% free!

Join the Coq Track