.. Idris Manual documentation master file, created by
   sphinx-quickstart on Sat Feb 28 20:41:47 2015.
   You can adapt this file completely to your liking, but it should at least
   contain the root `toctree` directive.

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/


* :ref:`tutorial-index`
* :ref:`eff-tutorial-index`
* :ref:`faq-index`
* :ref:`proofs-index`
* :ref:`reference-index`
* :ref:`guides-index`


.. _tutorial:

###################
The Idris Tutorial
###################

.. toctree::
   :maxdepth: 1

   tutorial/introduction
   tutorial/starting
   tutorial/typesfuns
   tutorial/classes
   tutorial/modules
   tutorial/packages
   tutorial/interp
   tutorial/views
   tutorial/theorems
   tutorial/provisional
   tutorial/interactive
   tutorial/syntax
   tutorial/miscellany
   tutorial/conclusions

.. _faq:

##########################
Frequently Asked Questions
##########################

.. toctree::
   :maxdepth: 1

   faq/faq

.. _effects:

################
Learning Effects
################

.. toctree::
   :maxdepth: 1

   effects/introduction
   effects/state
   effects/simpleeff
   effects/depeff
   effects/impleff
   effects/hangman
   effects/conclusions
   effects/summary

.. _proofs:

###############
Theorem Proving
###############

.. toctree::
   :maxdepth: 1

   proofs/pluscomm
   proofs/inductive
   proofs/patterns
   proofs/interactive

.. _reference:

##################
Language Reference
##################

.. toctree::
   :maxdepth: 1

   reference/documenting
   reference/uniqueness-types
   reference/ffi
   reference/erasure

.. _guides:

############
Short Guides
############

.. toctree::
   :maxdepth: 1

   guides/type-providers-ffi