Idris is a research-backed verification-aware programming language. Originally developed at the University of St Andrews, Idris is a general purpose functional programming language that supports dependent types. Since its inception Idris has gone through at least one major change, Idris(2) improved the Idris language by supporting quantities and made Idris(2) self-hosting.
To make life easier, we will refer to Idris(2) as just Idris.
In this section we will provide:
a brief overview of features common to all Idris versions;
some resources to help you learn more about Idris itself;
a quick note about interactive editing and why it is important when working with Idris;