Glad that I'm not the only one who hacked last test case around.
It really should have been a different kata because it made it one kyu harder than translations in other languages.

You forgot to add "do not be so stupid to do this in haskell" disclaimer!

Translating this Kata from Haskell into Coq/Idris/Agda was a mistake in the first place. But now that it's available in Coq/Idris/Agda, the only sensible thing to do is to lower its rank to match that of the language version in which it is easiest to complete this Kata in, because any rational future solver would choose the easiest path to completion.

I have already included notices in the descriptions of the remaining Haskell "theorem-proving" Kata explicitly asking translators not to make the same mistake by translating them into Coq/Idris/Agda, so rest assured you can complete, e.g. "A + B = B + A? Prove it!", and be 99.99% certain that it will never be re-ranked, to, say, 7 kyu.

P.S. I think Lensmaker kata is overrated because I've read "Optics by example". Can we fix that?

If you think that some Haskell Kata are overranked (and I'm sure quite a few people do), feel free to open an Issue requesting for re-ranking them on the Codewars GitHub repo, just like I did for Coq.

P.S. I understand your frustration of losing honor and rank progress overnight as a result of these re-rankings, and to be honest, I was initially opposed to it as well (just ask @Voile - I was one of the few people who deliberately overranked theorem-proving Kata in the first place, purely out of selfish interest). But then I realized that my actions were not helping the theorem-proving community on Codewars but rather damaging it, by making the rank of theorem-proving Kata useless in determining its actual difficulty. Think of the re-rankings as for the greater good - at least for Coq, now that the re-rankings are complete, it's finally ready to leave Beta (since 8-9 months ago when it was first added to Codewars) as a stable supported language on Codewars.

You forgot to add "do not be so stupid to do this in haskell" disclaimer! How come, it surely needs to be fixed. Otherwise one would be mad because of his lost fairly obtained points. Other than that, I am very grateful for your work! The platfrom's very essence is now eulogized by the fact that some insidious coq programmer (1 out of 1000000000000000000000000000000000000000000000000000000000000000000000, according to my precise calculations) would not obtain disproportionated points for this matter. Thanks, спасибо, どうもありがとうございます, dziękuję bardzo!

P.S. I think Lensmaker kata is overrated because I've read "Optics by example". Can we fix that?

Note to moderators: This Kata is not yet ready for re-approval. Its current average assessed rank is 3 kyu but we need to bring it down to at most 5 kyu before it can be considered for re-approval.

I mean, do you realize what you wrote meant? It was literally 'there is a type in universe level ℓ such that if this type is drinking, then every type in universe level ℓ is drinking'.

Thanks for your translation! I'm not familiar with Coq. So there is a little question. Is there a reason to have r of nat -> Prop? Can this type be more general?

It's not about size. In point-free version

`cycle "10"`

will most likely be evaluated only once (even if you don't really need it in this case)This comment is hidden because it contains spoiler information about the solution

Approved

Glad that I'm not the only one who hacked last test case around.

It really should have been a different kata because it made it one kyu harder than translations in other languages.

Lean Translation Kumited - please accept :-D

Translating this Kata from Haskell into Coq/Idris/Agda was a mistake in the first place. But now that it's available in Coq/Idris/Agda, the only sensible thing to do is to lower its rank to match that of the language version in which it is easiest to complete this Kata in, because any rational future solver would choose the easiest path to completion.

I have already included notices in the descriptions of the remaining Haskell "theorem-proving" Kata explicitly asking translators

notto make the same mistake by translating them into Coq/Idris/Agda, so rest assured you can complete, e.g. "A + B = B + A? Prove it!", and be 99.99% certain that it will never be re-ranked, to, say,`7 kyu`

.If you think that some Haskell Kata are overranked (and I'm sure quite a few people do), feel free to open an Issue requesting for re-ranking them on the Codewars GitHub repo, just like I did for Coq.

P.S. I understand your frustration of losing honor and rank progress overnight as a result of these re-rankings, and to be honest, I was initially opposed to it as well (just ask @Voile - I was one of the few people who deliberately overranked theorem-proving Kata in the first place, purely out of selfish interest). But then I realized that my actions were not helping the theorem-proving community on Codewars but rather damaging it, by making the rank of theorem-proving Kata useless in determining its actual difficulty. Think of the re-rankings as for the greater good - at least for Coq, now that the re-rankings are complete, it's finally ready to leave Beta (since 8-9 months ago when it was first added to Codewars) as a stable supported language on Codewars.

You forgot to add "do not be so stupid to do this in haskell" disclaimer! How come, it surely needs to be fixed. Otherwise one would be mad because of his lost fairly obtained points. Other than that, I am very grateful for your work! The platfrom's very essence is now eulogized by the fact that some insidious coq programmer (1 out of 1000000000000000000000000000000000000000000000000000000000000000000000, according to my precise calculations) would not obtain disproportionated points for this matter. Thanks, спасибо, どうもありがとうございます, dziękuję bardzo!

P.S. I think Lensmaker kata is overrated because I've read "Optics by example". Can we fix that?

Average assessed rank is now down to

`5 kyu`

Note to moderators: This Kata is not yet ready for re-approval. Its current average assessed rank is

`3 kyu`

but we need to bring it down to at most`5 kyu`

before it can be considered for re-approval.See: Codewars/codewars.com#2001

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

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

I mean, do you realize what you wrote meant? It was literally 'there is a

typein universe level ℓ such that if thistypeis drinking, then everytypein universe level ℓ is drinking'.`nat`

is just a random inhabited type. If you want to, I can change it to accept any inhabited type, but...Using

`Set ℓ`

isn't 'more general'; it's just weird.Thanks for your translation! I'm not familiar with Coq. So there is a little question. Is there a reason to have

`r`

of`nat -> Prop`

? Can this type be more general?Coq translation https://www.codewars.com/kumite/5e3ea2cacc92260029e246d2?sel=5e3ea2cacc92260029e246d2

## Loading more items...