G. Allais

Worth noting we have lambda-case thanks to #244

Note that you can use rlwrap to cope with the current limitations

Yep the files have holes for the exercises you're supposed to solve yourself :D

> Am I doing something wrong? I don't think so. As I said in the original message: I ported the code using the development version of Idris2 I had at...

Have fun!

This looks like insertion sort to me.

Thanks for the investigation Andreas, I had no idea where to start!

I haven't opened a PR for this yet

Yeah I'm afraid this will conflict hard with the new core. And so given the merge strategy edwin is planning to use (basically: overwrite current idris2 with his fork), we...

Interesting. Last time we had a similar error (pattern variables remaining at runtime) it was because of a use of rewrite but you don't seem to have any in your...