Coq

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

0 Mentors

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

13 Students

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

3 Exercises

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

About Coq

Join the Coq track
Require Import Coq.Strings.String.

Open Scope string_scope.

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

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

Exercism is a great website

What I like about it is that I am able to solve the challenges in a TDD way working in a environment that I am familiar (my own PC not a browser IDE) and the cherry on the top of the cake is that I have access to code reviews.

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.

Rna Transcription
medium
easy
misc
Hello World
medium
easy
misc
Tautology
medium
easy
misc

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

Join the Coq Track