The Coq mailing list

[Donald Leung <i.donaldl AT me.com>]

@Agnishom: Many thanks for your feedback and links to similar websites hosting recreational theorem-proving challenges. Unfortunately, since the Codewars platform was designed to support a wide variety of programming languages, the maintainers decided that it was impractical to support Coq-specific IDE features such as interactively stepping through a proof script. The current recommended way of solving a Coq challenge on Codewars is to simply copy the provided template into an IDE of your choice such as CoqIDE or Proof General and develop your solution locally. The preloaded code is often displayed within the Kata description itself so you may wish to copy those code snippets into your local environment as well in a separate file “Preloaded.v”.

@Vincent: The “omega” tactic (as is the rest of the Coq standard library plus a few external libraries) is available on Codewars - you can use it in your solution by adding “From Coq Require Import omega.Omega” to the top of your solution file.

More information about the Coq environment on Codewars can be found at https://github.com/Codewars/codewars.com/wiki/Language-Coq

Cheers,

Donald