-
Notifications
You must be signed in to change notification settings - Fork 221
Language Coq
Beta
8.9.0
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):
Goal True.
check_type Solution.my_theorem my_type.
Abort.Furthermore, if the user solution (e.g. Solution.my_theorem) is expected to be Closed under the global context then Print Assumptions Solution.my_theorem. may be used in place of the assertions provided by coq_codewars.
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.
12 seconds
None