Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker.
[6] Compared to Agda and Coq, Idris prioritizes management of side effects and support for embedded domain-specific languages.
Idris compiles to C (relying on a custom copying garbage collector using Cheney's algorithm) and JavaScript (both browser- and Node.js-based).
There are third-party code generators for other platforms, including Java virtual machine (JVM), Common Intermediate Language (CIL), and LLVM.
[7] Idris is named after a singing dragon from the 1970s UK children's television program Ivor the Engine.