The is the Idris Tutorial. It will teach you about programming in 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/
.. toctree:: :maxdepth: 1 introduction starting typesfuns interfaces modules packages testing interp views theorems provisional interactive syntax miscellany conclusions