Okay… for some strange reasons, Idris isn’t reducing my terms and keep a huge piece of unprocessable garbage instead of a String. But... if I enclose the content in a local definition in the REPL (:let foo = garbage) then it can process it.
-
Show this thread
-
Replying to @BeRewt
Curious. Is everything total, and public export? They are the most common reasons it might go wrong.
4 replies 0 retweets 1 like -
Replying to @edwinbrady
It was a public export in a function of a third party library. I don’t get why it was problematic though…
1 reply 0 retweets 0 likes
Replying to @BeRewt
If it was public export, but imported via some other library (so not directly) that might cause it. Reduction at the REPL is less restricted
8:08 AM - 30 Jan 2018
0 replies
0 retweets
0 likes
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.