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.
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.
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/
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.