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.
Very instructive Kata! Thanks!!
It is necessary to add to the condition that the Euclidean distance must be rounded down before comparing with the radius, otherwise this was not initially described in any way.
I was fortunate that I have some experience proving things in Agda; it definitely helped me here.
For those who were struggling on getting Haskell to type check, I was able to get predictable results once I realized that any expression of (NextOdd m) or (NextEven m) was S^2 of some m, and that I also knew the parity of m by definition. Then I could just unfold the expressions in terms of n or m using the exact definitions for Mult and Add on paper for the cases I was considering, keeping in mind the nesting. Because it is trivial to determine the parity of all the terms in the expression, once I had the "shape" of the unfolded expressions on paper, it was just a matter of using the lemmas we already proved to recompose the expression in the form of the lemma analogs we defined for arithmetic, working from the innermost nested expression outward. Hope that made some sense. This was a fun kata, and bumped my score by 2 kyu.
Would have been even kinda easy if I knew Haskell on any acceptable level. Most struggles were to make types work out and complie : |
Why is Idris an option here? there is an Idris equivalent of this problem that is only 7 KYU
nvm, never thought changing a variable's position matters
This comment is hidden because it contains spoiler information about the solution
I have a problem while attempting my code
The error is : "Import declarations must hide Unsafe.Coerce"
BTW I have used:
import Data.Coerce
import Unsafe.Coerce
import Data.Typeable
import Data.Type.Equality
Still showing the error.
Can anyone solve this bug :)
This fork should solve all issues:
Updated to Node v14
Approved
Approved
COBOL translation.
Lua translation pending approval.
This kata is really interesting!!!!!!! (After getting hands on some coq)
Loading more items...