• solomonirailoacommented on "Odd + Even = Odd? Prove it!" kata

Cool. How did you get the multiplication parts working? I'm kinda stuck with oddTimesOdd and oddTimesEven.

• csaltachincommented on "A+B=B+A? Prove it!" kata

But professor, my induction is correct! It compiled in Haskell!

Uhh, hard

• phonicsscommented on "Convert all the cases!" kata

My code c++ passed all tests.
But I am gtting error from random test: Caught std::exception, what(): std::bad_alloc
What is that mean?

done.

• JohanWiltinkcreated an issue for "Template Haskell: Tuple maker" kata

Needs update to `GHC 9.2.x`

• JohanWiltinkcreated an issue for "A+B=B+A? Prove it!" kata

Needs update to `GHC 9.2.x`

• RealKenshirocommented on "Odd + Even = Odd? Prove it!" kata

Very instructive Kata! Thanks!!

• Krillancreated a suggestion for "Draw a Circle." kata

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.

• lanebraincommented on "Odd + Even = Odd? Prove it!" kata

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.

• quilircommented on "Odd + Even = Odd? Prove it!" kata

Would have been even kinda easy if I knew Haskell on any acceptable level. Most struggles were to make types work out and complie : |

• Trouble-Trufflecommented on "Odd + Even = Odd? Prove it!" kata

Why is Idris an option here? there is an Idris equivalent of this problem that is only 7 KYU

• lllsssskkkresolved a question on "Odd + Even = Odd? Prove it!" kata

nvm, never thought changing a variable's position matters

• lllsssskkkcreated a question for "Odd + Even = Odd? Prove it!" kata

This comment is hidden because it contains spoiler information about the solution