Idris combines a number of features from relatively mainstream functional programming languages with features borrowed from proof assistants.
Idris combină o serie de caracteristici din limbile de programare funcționale relativ importante, cu caracteristici împrumutate de la asistenții de probă.