Language Reference

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/

• Documenting Idris Code
• Packages
• Uniqueness Types
• New Foreign Function Interface
• Syntax Guide
• Erasure By Usage Analysis
• The IDE Protocol
• Semantic Highlighting & Pretty Printing
• DEPRECATED: Tactics and Theorem Proving
• The Idris REPL
• Compilation and Logging
• Core Language Features
• Language Extensions
• Elaborator Reflection
• Miscellaneous