Uma visão geral de como começar do zero com o Idris
Este tutorial pretende ser uma breve introdução à linguagem e destina-se a leitores que já conhecem uma linguagem funcional como Haskell ou OCaml. Em particular, assume-se uma certa familiaridade com a sintaxe de Haskell, embora a maioria dos conceitos seja pelo menos explicada de forma breve. Assume-se também que o leitor tem algum interesse em usar tipos dependentes para escrever e verificar software de sistemas.