This is the reference guide for the Idris Language. It documents the language specification and internals. This will tell you how Idris works, for using it you should read the Idris Tutorial.
Note
The documentation for Idris has been published under the Creative Commons CC0 License. As such to the extent possible under law, The Idris Community has waived all copyright and related or neighboring rights to Documentation for Idris.
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
codegen documenting packages uniqueness-types ffi syntax-guide erasure ide-protocol semantic-highlighting tactics repl compilation internals language-features language-extensions elaborator-reflection type-directed-search partial-evaluation misc