Nice kata, and nice translation! Here is a fork restricting the imports of the tests and preloaded to only .Base for some modules (which is all they need anyway). It should make it much more feasible to pass this kata on 2.6.2.

As a kata author, I greatly appreciate when someone else approves a translation of one of my katas, or updates the kata to comply with newer language versions or testing framework, as long as the kata is not distorted in any manner.

Based on this, I rejected the fork. A new fork can adjust the tests.

There are also even tools for making your own solutions in this style: https://pointfree.io/

So I have started working on this now, and I am kind of enjoying the challenge of figuring out how the other players logic works. Having said that, mentioning that they aren't just random players might be nice.

Last week. Also going through the LC kata's. BF and NASM will follow soon. I decided to no longer just solve in Codewars Editor, but use IDE's and local sandbox environments.

Nice! Since when have you been solving Agda kata btw?

Ok I passed. For me, knowing there is a workaround is fine. Up to you to decide whether to factor out the heavy lib import for this kata :)

ok I'm making local copies, thanks. Wait with your edits, let me try the first approach first.

No, though the newer version of Agda is notoriously very slow, due to its std-lib being much larger than the previous version. This means that some large modules will cause timeout just by importing them.

I have been trying to get the Agda timeout raised to 30s, but no luck so far. In the meantime a workaround is to copy individual definitions from the std-lib to avoid expensive imports. It is quite annoying. I know monadius has said he will not solve any more Agda kata until the timeout issue is resolved.

Unfortunately I cannot enable the older version for this kata because the Permutation relation used here does not exist in the older version... Hm, or maybe I could just define it myself. Maybe I will do that actually.

Are there perf constraints?

Should be O(nlogn)

Thanks for this comment, finally reminded me to come back and solve this!

I don't know what the current state of messaging is to users as they gain additional site privileges, but I can say from my own experience that I recall it being very confusing. Without any guidance being told "you can now create/edit XYZ on the site" is disorienting (should I be editing this?). The system seems to be mostly upheld by community expectations, rather than explicit instructions, but even those don't have a centralized source and seem to be learned piecemeal from experience.

"Any person's count" does not specify a time, because it is not specific to a time. At any time, the persons count is a count of everyone currently at the party, including themselves.

"Any person's count of people who will stay includes themself."

This would be inaccurate, since they do not count people based on if they will stay, they count everyone currently at the party. If people leave, then the count changes. Also that wording would imply that they are amongst the people who will stay, meaning no one would ever leave.

I adapted it slightly to "Any person's count of people currently at the party includes themself.", and added it to the description. Is that OK?