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

• Introduction
• Getting Started
• Types and Functions
• Type Classes
• Modules and Namespaces
• Packages
• Example: The Well-Typed Interpreter
• Views and the “with” rule
• Theorem Proving
• Provisional Definitions
• Interactive Editing
• Syntax Extensions
• Miscellany
• Further Reading

Frequently Asked Questions

• Frequently Asked Questions

Learning Effects

• Introduction
• State
• Simple Effects
• Dependent Effects
• Creating New Effects
• Example: A “Mystery Word” Guessing Game
• Further Reading
• Effects Summary

Theorem Proving

• Running example: Addition of Natural Numbers
• Inductive Proofs
• Pattern Matching Proofs
• Interactive Theorem Proving

Language Reference

• Documenting Idris Code
• Uniqueness Types
• New Foreign Function Interface
• Erasure By Usage Analysis
• The IDE Protocol

Short Guides

• Type Providers in Idris