This article represents my first attempt to get up and running with the Idris programming language. It will document not only how to make an executable Idris package but also the basics of what Idris is and why it's not like any other programming language you're likely to have used before. From a practical perspective, it will cover some basic syntax as well as how to compile and run an Idris 2 program, including .ipkg usage. Unlike most other Idris learning resources, I will not assume you alre...