exercism/coq

Name: coq

Owner: exercism

Description: Exercism exercises in Coq.

Created: 2017-05-05 17:48:45.0

Updated: 2017-10-19 07:51:14.0

Pushed: 2017-10-23 03:30:57.0

Homepage: http://exercism.io/languages/coq

Size: 31

Language: Coq

GitHub Committers

UserMost Recent Commit# Commits

Other Committers

UserEmailMost Recent Commit# Commits

README

Exercism Coq Track

Build Status

Exercism exercises in Coq.

Setup

There are 2 ways to install Coq:

  1. [Recommended] Using OPAM package manger: https://coq.inria.fr/opam/www/using.html
  2. [Alternative] Directly download Coq binaries from the official site: https://coq.inria.fr/download

For editing Coq sources we recomend using one of the following:

  1. [Recommended] Emacs editor with ProofGeneral and CompanyCoq. See https://github.com/cpitclaudel/company-coq for installation instructions.
  2. [Alternative] Using CoqIDE

Presently, exercises do not require any additional Coq libraries. Recommended version of Coq: 8.6

Contributing

Thank you so much for contributing! :tada:

Please read about how to get involved in a track. Be sure to read the Exercism Code of Conduct.

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.

Exercise Tests

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:

rem TautologyExercise: True.
f.
 Add your proof here *)

Opening an Issue

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.

Submitting a Pull Request

Pull requests should be focused on a single exercise, issue, or conceptually cohesive change. Please refer to Exercism's pull request guidelines.

Verifying Your Change

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

DO: add this command

For the Exercism-specific linting, please see the documentation.

Contributing a New Exercise

Please see the documentation about adding new exercises.


This work is supported by the National Institutes of Health's National Center for Advancing Translational Sciences, Grant Number U24TR002306. This work is solely the responsibility of the creators and does not necessarily represent the official views of the National Institutes of Health.