Un aperçu de la façon de se lancer dans Idris depuis zéro
Ce tutoriel se veut une brève introduction au langage, et il s'adresse à des lecteurs qui connaissent déjà un langage fonctionnel tel que Haskell ou OCaml. On y suppose en particulier une certaine familiarité avec la syntaxe de Haskell, même si la plupart des concepts y sont au moins expliqués brièvement. On suppose également que le lecteur s'intéresse quelque peu à l'utilisation des types dépendants pour écrire et vérifier des logiciels système.