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: https://creativecommons.org/publicdomain/zero/1.0/
- Code Generation Targets
- Documenting Idris Code
- Packages
- Uniqueness Types
- New Foreign Function Interface
- Syntax Guide
- Syntax Reference
- Erasure By Usage Analysis
- The IDE Protocol
- Semantic Highlighting & Pretty Printing
- DEPRECATED: Tactics and Theorem Proving
- The Idris REPL
- Compilation, Logging, and Reporting
- Idris’ Internals
- Core Language Features
- Language Extensions
- Type Directed Search
:search
- Static Arguments and Partial Evaluation
- Miscellaneous