Edwin Brady
Edwin Brady
The only plausible explanation I can come up with for a deeply nested name on reading (it turns out to be (NS [] (NS [] (NS [] ...))) is that...
I believe I've found the cause of this. I encountered the same problem, but in an easier to reproduce way! There was an allocation error when writing out ttc files....
Yes, I run through `rlwrap` (in fact I've aliased `idris2`). This is a fairly big feature request, in practice, requiring readline support or similar, and then leads to wanting tab...
You can't use `f` there because of the type of `>>=`, which is unrestricted in its second argument. There's still some glitches in the calculation of quantities in holes under...
yes, that error message isn't very good, but it'll take a bit more work to come up with a clearer one I think - since it depends a bit on...
Hi, thanks for doing this! My main worry about it is that I only know slightly more than nothing about Docker (that user is unlikely to be me unless I...
I don't think they should, because the body of the let should be indented further right than the `u`. Actually I think `x5` should also be rejected but I can...
If this is to do with the Mac chez test failures, perhaps it's okay now?
There's a test failure here due to the prelude change (I should do something about the line number display there, it is fairly useless.) Still, I'm not sure this should...
Sorry to be so slow at noticing this, I'm not keeping up with this repo. `a` is expected, though - `b` used to work for adding the body of an...