Documentation for the Idris 2 Language
Note
The documentation for Idris 2 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/
- A Crash Course in Idris 2
- Frequently Asked Questions
- Compiling to Executables
- Changes since Idris 1
- Type Driven Development with Idris: Updates Required
- Packages
- Where To Find Libraries
- Structuring Idris 2 Applications
- Foreign Function Interface
- Theorem Proving
- Implementation Notes
- Idris2 Reference Guide
- Cookbook