Documentation for the Idris Language¶
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/
- The Idris Tutorial
- The Effects Tutorial
- Frequently Asked Questions
- Theorem Proving
- Language Reference
- Tutorials on the Idris Language
The Idris Tutorial¶
Frequently Asked Questions¶
Learning Effects¶
Theorem Proving¶
Language Reference¶
- Documenting Idris Code
- Packages
- Uniqueness Types
- New Foreign Function Interface
- Syntax Guide
- Erasure By Usage Analysis
- The IDE Protocol
- Semantic Highlighting & Pretty Printing
- The Idris REPL
- Tactics and Theorem Proving
- Compilation and Logging
- Core Language Features
- Language Extensions
- Elaborator Reflection
- Miscellaneous