@@ -314,24 +314,32 @@ paths through the material can be found in the file `deps.html`.
314314
315315=== System Requirements
316316
317- \t odo[inline]{Rewrite this for Idris}
317+ Idris runs on Windows, Linux, and macOS. You will need:
318318
319- Coq runs on Windows, Linux, and OS X. You will need:
319+ - A current installation of Idris, available from
320+ \href{https://www.idris-lang.org/}{the Idris home page}. Everything should
321+ work with version 1.0. (Version 1.1.0 should work, but hasn't been tested by
322+ the Idris translation maintainers.)
320323
321- - A current installation of Coq, available from the Coq home page. Everything
322- should work with version 8.4. (Version 8.5 will _not_ work, due to a few
323- incompatible changes in Coq between 8.4 and 8.5.)
324+ - A supported editor for interacting with Idris. Currently, there are (at
325+ least) five choices:
324326
325- - An IDE for interacting with Coq. Currently, there are two choices:
327+ - \href{https://github.com/idris-hackers/atom-language-idris}{atom-language-idris}:
328+ An Idris Mode for Atom.io
326329
327- - Proof General is an Emacs-based IDE. It tends to be preferred by users who
328- are already comfortable with Emacs. It requires a separate installation
329- (google " Proof General " ).
330+ - \href{https://github.com/idris-hackers/idris-mode}{idris-mode}:
331+ Idris syntax highlighting, compiler-supported editing, interactive REPL
332+ and more things for Emacs
330333
331- - CoqIDE is a simpler stand-alone IDE. It is distributed with Coq, so it
332- should " just work" once you have Coq installed. It can also be compiled
333- from scratch, but on some platforms this may involve installing additional
334- packages for GUI libraries and such.
334+ - \href{https://github.com/idris-hackers/idris-sublime}{idris-sublime}:
335+ A Plugin to use Idris with Sublime
336+
337+ - \href{https://github.com/idris-hackers/idris-vim}{idris-vim}:
338+ Idris mode for vim
339+
340+ - \href{https://github.com/zjhmale/vscode-idris}{idris-vscode}:
341+ Idris for Visual Studio Code
342+ \url{https://marketplace.visualstudio.com/items?itemName=zjhmale.Idris}
335343
336344=== Exercises
337345
0 commit comments