Coq 8.15 should be enabled.
Pretty frustrating that you basically have to to know that a certain function exists in order to do this...
For ease of working in an IDE, the entirety of the preloaded section should be in a single codeblock at the end of the description or as a comment in the solution setup.
The link to the paper in the description is broken. Here's a working one:
https://mbodin.github.io/esplorado/itp13.pdf
Fun Kata :)
Freaking prelude! There should be a second solution for this!
Tedious (at least for me), but definitely not 1kyu
I completely agree, this seems significantly easier than some of the other 4-kyu ranked puzzles out there. 6-kyu would seem more adequate.
Do you still get the error? I tried to run it and it worked
Approved :)
Loading collection data...
Coq 8.15 should be enabled.
Pretty frustrating that you basically have to to know that a certain function exists in order to do this...
For ease of working in an IDE, the entirety of the preloaded section should be in a single codeblock at the end of the description or as a comment in the solution setup.
The link to the paper in the description is broken. Here's a working one:
https://mbodin.github.io/esplorado/itp13.pdf
Fun Kata :)
Freaking prelude! There should be a second solution for this!
Tedious (at least for me), but definitely not 1kyu
I completely agree, this seems significantly easier than some of the other 4-kyu ranked puzzles out there. 6-kyu would seem more adequate.
Do you still get the error? I tried to run it and it worked
Approved :)
Loading more items...