Language Coq

Status

Beta

Versions

8.9.0

Test Frameworks

coq_codewars

There is also a check_type tactic that can be used to check the type of the user solution as follows (assume Solution.my_theorem is the user solution and my_type is the type that it should have):

(* Include this at the beginning of the test suite to use the check_type tactic *)
Require Import Check.

Goal True.
  check_type Solution.my_theorem my_type.
Abort.

Interactive Proof Editing Support

Unfortunately, the Codewars environment does not support the interactive development of Coq proofs. The current recommended method of solving a Kata is by copying the relevant code snippets onto your local machine and developing your solution locally: preloaded code should go into Preloaded.v, your solution into Solution.v and the Sample/Submit tests into Tests.v.

Timeout

12 seconds

Packages

• Equations
• TLC
• mathcomp

Services

None