Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but it is designed to be a general-purpose programming language similar to Haskell.
The Idris type system is similar to Agda's, and proofs are similar to Coq's, includi...