Closed shmish111 closed 6 years ago
hi @shmish111 you will be interested in Idris' support for packages.
http://idris.readthedocs.io/en/latest/tutorial/packages.html
Idris Mode is package aware.
The way to do this is indeed to use a package. If this doesn't work for you, please re-open the issue.
If I have a project based in a folder called src, I need to tell idris by passing the
-i
parameter, e.g.idris -i src
however there seems to be no way I can do this in idris mode. This means I cannot use interactive environment for a file that imports another module in my project. Is there some way to pass this parameter to the idris process in idris mode?