Language Reference — Idris 1.0 documentation

# 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/

- Code Generation Targets
- 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, Logging, and Reporting
- Idris’ Internals
- Core Language Features
- Language Extensions
- Elaborator Reflection
- Type Directed Search `:search`
- Static Arguments and Partial Evaluation
- Miscellaneous