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! 😭

<*> is a better fit than >>= for zipWith .. tail. When fed an empty list, zipWith (*) [] (tail []) returns [] without evaluating tail []. zipWith (*) (tail []) [] crashes. That's why you want the second list to be shorter, thus <*>.

In this case, maximum [] will crash anyway, so it doesn't matter, you need a list of at least two elements to succeed at all.

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

Fixed

GHC 8.8.4 (which is the default version)

Sample test returns:

But same runs in 8.2.2(sample and full) and 8.8.4(only full) fine.

that shocking me

I absolutely hated doing that, but I'm really glad I did :)

I thought that

give upmeant I was supposed to usefold!Haha, now that really sent me barking down the wrong alley...

`<*>`

is a better fit than`>>=`

for`zipWith .. tail`

. When fed an empty list,`zipWith (*) [] (tail [])`

returns`[]`

without evaluating`tail []`

.`zipWith (*) (tail []) []`

crashes. That's why you want thesecondlist to be shorter, thus`<*>`

.In this case,

`maximum []`

will crash anyway, so it doesn't matter, you need a list of at least two elements to succeed at all..

## Loading more items...