Una visión general de cómo empezar desde cero con Idris
Este tutorial pretende ser una breve introducción al lenguaje y está dirigido a lectores que ya estén familiarizados con un lenguaje funcional como Haskell u OCaml. En concreto, se presupone cierta familiaridad con la sintaxis de Haskell, aunque la mayoría de los conceptos se explicarán al menos brevemente. También se presupone que el lector tiene cierto interés en usar tipos dependientes para escribir y verificar software de sistemas.