0.5 is not a natural number.

Even * anything not always equal even
example: 2*0.5 = 1

Unpublishing due to very low satisfaction rating and many unresolved issues.

Free points! :)

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.

Mhm... That's confusing. I've ran into the same issue with other Kata that use random tests. Is there something that I've done wrong?

I am surprised: I tried the two existing solutions and they worked fine without errors or warnings. Unfortunately your solution gives wrong results.

Nim tests are broken, as some things have been deprecated.

/workspace/solution_tests.nim(63, 7) template/generic instantiation of `suite` from here
/workspace/solution_tests.nim(65, 35) Warning: Deprecated since v0.18.0; use 'rand' instead; random is deprecated [Deprecated]
/workspace/solution_tests.nim(63, 7) template/generic instantiation of `suite` from here
/workspace/solution_tests.nim(66, 35) Warning: Deprecated since v0.18.0; use 'rand' instead; random is deprecated [Deprecated]
/workspace/solution_tests.nim(70, 7) template/generic instantiation of `suite` from here
/workspace/solution_tests.nim(72, 35) Warning: Deprecated since v0.18.0; use 'rand' instead; random is deprecated [Deprecated]
/workspace/solution_tests.nim(70, 7) template/generic instantiation of `suite` from here
/workspace/solution_tests.nim(73, 35) Warning: Deprecated since v0.18.0; use 'rand' instead; random is deprecated [Deprecated]
Error: execution of an external program failed: '/workspace/tests '

Alright I see. I've yanked the kata at the moment, since this question is from somewhere else, and I might need to get their permission before publishing it.

Consistency is a good thing to have but it is not covenient to work with rational numbers in Coq. They do not support the standard equality and one has to use a setoid-based equality to reason about rational numbers (and this equality has some limitations). In any case, I think it would be better to change everything to real numbers because arctan is usually defined as a function from reals to reals.

P.S. I didn't reply earlier because I did not get a notification about your comment.

Coq Translation Kumited - please accept :-D