Closed joelberkeley closed 3 years ago
You need to install the idris2api along with the idris2 compiler itself, here's how https://github.com/idris-lang/Idris2/blob/master/INSTALL.md#7-optional-installing-the-idris-2-api
You can add that to the docs if you want, otherwise I will when I next get round to coding.
ok, thanks. Will that always be the case or will plain Idris do in the future?
Unless there's a change to idris2 itself, I believe so, because Inigo needs some functions and data types from the idris2 source code. It's good to rely on idris2api so if there's a change, we have to keep up with it. I might try getting downloads to work with github CI, so you might be able to use that in future
I cloned the repo and followed the installation instructions, but I get
even though I have idris2 installed (if I run
idris2
in the terminal I get the REPL)