Suppose I have a type function Eff () [STDIO]
in Idris. This allows you to perform basic I / O operations in the console, but does not allow you to use the Idris external function interface.
Is there an effect in idris that allows you to do this or some other way around this problem? I do not want to use IO
, as in this example , since I would like to mix FFI with other effects. So, if I wanted to use the FFI and the effect of the state, for example, I would like to use the type: Eff () [FFI,State Int]
. Is this possible in the current implementation of Idris?
source
share