Exercism exercises in Coq.
There are 2 ways to install Coq:
For editing Coq sources we recomend using one of the following:
Presently, exercises do not require any additional Coq libraries. Recommended version of Coq: 8.6
Thank you so much for contributing! 🎉
We welcome pull requests of all kinds. No contribution is too small.
We encourage contributions that provide fixes and improvements to existing exercises. Please note that this track's exercises must conform to the Exercism-wide standards described in the documentation. If you're unsure about how to make a change, then go ahead and open a GitHub issue, and we'll discuss it.
At the most basic level, Exercism is all about the tests. You can read more about how we think about test suites in the Exercism documentation.
Test files should use the following format:
Theorem TautologyExercise: True. Proof. (* Add your proof here *) Qed.
If you plan to make significant or breaking changes, please open an issue so we can discuss it first. If this is a discussion that is relevant to more than just the Coq track, please open an issue in exercism/discussions.
Pull requests should be focused on a single exercise, issue, or conceptually cohesive change. Please refer to Exercism's pull request guidelines.
Before submitting your pull request, you'll want to verify the changes in two ways:
All the tests for Coq exercises can be run from the top level of the repo with
# TODO: add this command
For the Exercism-specific linting, please see the documentation.
Please see the documentation about adding new exercises.