The Idris Tutorial — Idris 1.0 documentation

# The Idris Tutorial

This is the Idris Tutorial. It provides a brief introduction to programming in the Idris Language. It covers the core language features, and assumes some familiarity with an existing functional programming language such as Haskell or OCaml.

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/

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