Idris is a general-purpose purely functional programming language with dependent types, strict or optional lazy evaluation and features such as a totality checker.
Idris este un limbaj de programare pur funcțional, cu scop general, cu tipuri dependente, evaluare lenească strictă sau opțională și caracteristici cum ar fi o verificare a totalității.