Loading collection data...
Collections are a way for you to organize kata so that you can create your own training routines. Every collection you create is public and automatically sharable with other warriors. After you have added a few kata to a collection you and others can train on the kata contained within the collection.
Get started now by creating a new collection.
This comment is hidden because it contains spoiler information about the solution
The Coq version of this kata requires a constructive proof.
Yeah, I think it would be somewhat interesting, but might also have negative side effects of spreading the misconception that constructive code is central to interactive theorem proving.
I see, thanks for explaining, thats a little unfortunate, would be cool to be able to actually test for constructive kata.
This comment is hidden because it contains spoiler information about the solution
This comment is hidden because it contains spoiler information about the solution
which solution?
This comment is hidden because it contains spoiler information about the solution
A good patch is to have
noncomputable theory
open_locale classical
in the header of any Lean kata which is meant to be about "everyday mathematics".
I don't think "learn Lean entirely through exercises on Codewars" is a particularly good life strategy, anymore than it would be for learning other languages. Come ask questions here
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members
or use this website to find reference material
https://leanprover-community.github.io/
I've edited the kata after authoring the translation so you might get a description merge conflict when trying to approve the original translation. In that case, you may wish to approve this fork instead.
Coq Translation Kumited - please accept :-D
This comment is hidden because it contains spoiler information about the solution
This comment is hidden because it contains spoiler information about the solution
I think this would be better with z:\R instead of z:\Z.