Idris
v0.9.18
  • 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
  • Introduction
  • State
  • Simple Effects
  • Dependent Effects
  • Creating New Effects
  • Example: A “Mystery Word” Guessing Game
  • Further Reading
  • Effects Summary
  • Running example: Addition of Natural Numbers
  • Inductive Proofs
  • Pattern Matching Proofs
  • Interactive Theorem Proving
  • Documenting Idris Code
  • Uniqueness Types
  • New Foreign Function Interface
  • Erasure By Usage Analysis
  • Type Providers in Idris
Idris
  • Docs »
  • Documentation for the Idris Language
  • Edit on GitHub

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

Short Guides¶

  • Type Providers in Idris
Next

© Copyright 2015, The Idris Community. Revision ad553427.

Built with Sphinx using a theme provided by Read the Docs.
Read the Docs v: v0.9.18
Versions
latest
stable
v0.9.20.2
v0.9.20.1
v0.9.20
v0.9.19.1
v0.9.19
v0.9.18.1
v0.9.18
Downloads
pdf
htmlzip
epub
On Read the Docs
Project Home
Builds

Free document hosting provided by Read the Docs.