lovely. interesting use of the list difference operator!
Wait, wha- 🤯
Okay: i feel stupid :)
also: i had some problems using them when i did the definition in ltac, for now i just copypasted the output from Show Proof.
i could not use the stream_unfold unless the definition was not in ltac.
Is there any reason odd is a Definition not a CoFixpoint?
I like that you used a list comprehension. I forget about those sometimes
Thanks. I do think "Modular operations" is overranked. It takes sometime to get familiar with Fin and then work with its tricky definition, but the overall solution is usually not long: mine is about 40 lines and it's a lot simpler if you know the mod function as in andersk's solution. So I'd say it should be 2 kyu, for someone who knows mod maybe it should even be 3 kyu. The rank for "String formatting" is about right, it takes time to get used to defining functions that work on types and come with up that idea for the Kata as a learner.
Inconsistent ranking is a well known Codewars issue. The "Modular operations" kata is overranked. There is an ongoing work to adjust ranks of Agda kata.
In my opinion, this kata is between 1 and 2 kyu. I approved it as 2 kyu because it has a Coq translation. And it is simpler to write proofs in Coq.
Assuming that this kata is 1.5 kyu in Agda, I would like to know your rank suggestions for the "Modular operations" kata and the "String formatting" kata. Since you are learning Agda, your rank suggestions will be very valuable.
I am currently learning Agda. I completed the 1 kyu Kata "Modular operations on Finite data type" and then started to try this Kata becasue I haven't learned Cubical Agda but I learned about this in our math lessons so I thought this would be easier to start with. However, it took me a lot more time than expected.
I defined the Cantor pairing function and its inverse in the primitive with only addition, substraction, and recursion. Then proving the bijection using well-founded induction is a lot trouble and took a lot of time. I thought maybe I myself made the problem more complicated than it should be in this way, but I took a rough look at some other solutions and they all turned out to be just as lengthy.
So just a suggestion: maybe this Kata should be ranked 1 kyu instead of 2 kyu to be less misleading, considering that I spent much more time to complete this than a 1 kyu Kata, that all the solutions I see seem to quite lengthy, and that the total times this has been completed is actually less than 3 of the 4 currently existing 1 kyu Agda Katas. Or possibly in the other way, maybe "Modular operations on Finite data type" should be ranked down since I see some really short solutions there.
And a tip for those who think this should be easy like I did: it is not, especially if it's your first time to use well-founded induction! 😭
The rank is adjusted