I really don't like the way scoping works in Idris. I feel like it tries to do too much automagically & just fails to understand what I mean
@eisaru Even so, can you show me your code? Error messages should explain this problem, and ought to have got better recently.
-
-
@edwinbrady After minimisation: this is broken http://lpaste.net/158422 and this works http://lpaste.net/158423 -
@eisaru That's certainly consistent with the rules…
- 4 more replies
New conversation -
-
-
@edwinbrady It's all fixed (I was working on the FreshList I sent to the ML). I have '0.9.19.1' so the error msgs may have gotten better ;) -
@eisaru oh. An ancient version, we're on 0.11 now. There could easily have been an error in the scoping rules implementation then.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.