Edwin Brady
Edwin Brady
This would be good to have, but it is indeed insertion sort. I'll merge once it's updated.
I think merge sort would be better, yes, just for the generally better performance - I think that is what you intended though isn't it?
Hmm, this is a bit awkward. The subtyping rules are to allow you to pass linear functions to HOFs which don't have linearity constraints (but not vice-versa). But this suggests...
Diamond shaped inheritance structures are awkward because implementations of the same interface aren't guaranteed to be equal. There's a bit of noise in the error message, but it looks like...
Yes, indeed, they are :). I should probably get around to implementing this sooner rather than later...
I get a crash due to stack overflow, it's interesting that you don't see that behaviour! Or maybe you compiled Idris2 with -O2 which might change one of the functions...
I suspect this is just that it's not checking whether there are holes left over after checking at the REPL (via `checkUserHoles`), and given that the missing argument isn't checked...
I'm not fussy about this one, to be honest - it feels like there ought to be a neater way to do it in any case (I'm not keen on...
That's right, `filter` isn't in the prelude, it's in `Data.List`.
This turns out to be because when we delay elaborators, we never check that the result type unifies with the expected type. Usually this is okay, because when we delay...