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.
I completely agree, this seems significantly easier than some of the other 4-kyu ranked puzzles out there. 6-kyu would seem more adequate.
Fixed
Fixed
Same for Coq. As far as I can tell there is no way to inspect the Preloded file, and the interface of codewards is completely inadequate. I managed to find the required definitions by Printing their names and "attempting" to solve the problem, which then shows the result of running the file. But this is really suboptimal.
Edit: Ok, my bad, the definitions are provided in the comments of the problem. This still strikes me as a weird way to do it.
This Kata is not compatible with Lean 3.20.c as of 08/10/2020
This Kata is not compatible with Lean 3.20.c as of 08/10/2020
Fixed
Fixed
This Kata is not compatible with Lean v3.18.4 as of 16/08/2020 and needs to be upgraded.
This Kata is not compatible with Lean v3.18.4 as of 16/08/2020 and needs to be upgraded.
The extra
cases nused here to make the-1s easier to get rid of is sweet! It's a very convenient way of replacing everynin a goal withn.succ.This comment is hidden because it contains spoiler information about the solution
No worries - just leave it for now then.
If this comment is addressed to me, I am not sure I am confident enough with Coq syntax any more to know whether what you have done is OK (I haven't used Coq for about 2 years and I quickly forget things which I don't use a lot).
Loading more items...