Edwin Brady
Edwin Brady
I'm pretty sure this (and Ohad's performance problem) are down to things from the prelude/base libraries not being evaluated, so blocking and causing huge terms that need quoting/writing out. Idris...
Yes, the `Extra` ones did leap out as being the most in need of organisation! I bet a lot of that belongs in the relevant base modules by now.
Thanks everyone for the comments so far. I'm going to leave this open for a bit and see what else comes on before I decide what to do. Some interesting...
I'm a bit surprised this gets past the positivity checker. I suppose we'd better fix that... At some point we should also get on with fixing `Type : Type`. Mostly...
Thanks for getting this working. I'm not really sure this is the right place for it though, especially given that I'm not in a position to maintain it (or even...
I think it's reasonable to allow interleavings of the two different `let` forms.
This does make the nat hack a bit less hacky, thanks! Is the compile time performance still an issue? Sometimes that can be due to ambiguity resolution going a bit...
It can't resolve the ambiguity of `toList`, although it doesn't say that explicitly. Idris 2 won't try to resolve ambiguities which rely on interface resolution, unlike Idris 1, so you...
(I don't actually know on first looking why `g` works, by the way...) EDIT: Yes I do, in fact, it's to do with when it reruns delayed elaboration problems (if...
Did you clean everything first? You might have an out of date `YafflePaths.idr`