Dependent types – Idris documentation
docs.idris-lang.org