Idris is pretty well documented. It feels pretty inaccessible when you're just looking at the code, but in an editor with a plugin (Emacs, Atom, Vim), everythin

Idris is pretty well documented. It feels pretty inaccessible when you're just looking at the code, but in an editor with a plugin (Emacs, Atom, Vim), everything can be inspected, and it feels much more alive that way. Editing dependently-typed code has a particular development style which is very interactive, in which you fill in "holes" (code to be written) with help the from the editor/type-checker, providing feedback and suggestions. Resources: http://docs.idris-lang.org/en/latest/tutorial/index.html http://docs.idris-lang.org/en/latest/tutorial/index.html https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i... https://github.com/idris-hackers/software-foundations https://github.com/idris-hackers/software-foundations https://www.youtube.com/watch?v=4i7KrG1Afbk https://www.youtube.com/watch?v=4i7KrG1Afbk