Could you tell me how? I have no idea how to test such things in Agda
The tests that check for the correctness of p+ assumes that it reduces on the left argument, but this is not necessarily required. It can be reduced on the right argument too. And there are probably even more ways to implement it that is correct by nevertheless will not be equal.
Actually that's another issue, raising it instead
Not sure what does that mean. Check how I tested p+ in Agda final test, maybe that's what are you looking for
This comment is hidden because it contains spoiler information about the solution
@Voile what's with Coq translation?
Anyway, if user does not import anything(as intended), there won't be any conflicts.
It's still in beta, and there are only 4 solves, it doesn't really matter at the moment...
I don't know what to do with it :(
In Preloaded I should probably explicitly import things in Relation.Binary.PropositionalEquality, or better - import it in Solution. But it's too late, because if I will do that now, everyone's solution won't be accepted.
(did you mean
There are apparently more stuff in Preloaded than just Painfulℕ? Why is Preloaded exposing the things it's imported?
Also, as ⇔ is using a custom definition than the one in built-in Function.Equivalence, it should be in the description too. In fact you should just post the entire Preloaded code instead of an ambiguous github gist link.
I believe @bredor just forgot to delete it.