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.
-
-
It was a public export in a function of a third party library. I don’t get why it was problematic though…
-
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
End of conversation
New conversation -
-
-
Public export should be okay. Totality might be an issue but I need to look at it again. What puzzles me is the different behaviour of :let
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Let me clean it a bit and I’ll post it.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Thanks for the guidance!
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.