Looks like in addition to 'Best Practice' and 'Clever' solutions I strongly would like to have the button 'OMG' or 'LOL' :). Anyway, appreciate the persistance of the author!
Great kata, had a lot of fun solving it but I would propose to choose a few operators you will be using and pointing them out in the description because in the end we are basically doing the same thing for every operator which is not as fun.
It's a CW bug or something, I just reported it. Did you click Fork? It's crazy x)
How come one of the solutions has a sorry?
Lean Translation Kumited - please accept :-D
I had the same issue at first. I don't know if you have the same issue, but give the following a thought:
What happens if you use your MagicCompare instance in a for loop's body for your comparison and then re-use it as your loop index.
Hope this helps ;)
Coq translation submitted.
Fixed by checking type of left, right and comm in the test.
Typo: IsCommuntative should be IsCommutative.
This comment is hidden because it contains spoiler information about the solution
You can open import Bla as B, and use B.bla to refer to its members.
open import Bla as B