Some guides for using for Idris are:
-
Pre-reading material for CS886, which is provided as part of the curriculum for the Postgraduate MSc degree CyberSecurity at the University of Strathclyde.
If you have not programmed using a functional language, let alone using dependent types, then the ‘Three-Times’ may be a good start.
A Crash Course in Idris2, Sections 1-7,9,11+;
The Idris2 ‘crash course’ is a useful quick introduction to the core concepts of dependently typed programming. The introduction, however, was designed primarily for those with a background in functional programming a la Haskell. So if you are completely new to functional programming then YMMV.
The Idris Communities’ Idris Tutorial
This tutorial provides a ‘comprehensive’ resource for learning Idris2. Please be aware that this tutorial is not necessarily geared towards the novice programmer nor those unaware of programming in a functional language.
-
The Idris book provides a long and gentle introduction to functional programming in a dependently-typed language. I acknowledge that reading it appears to be a lot of work, but the long and gentle introduction will help with your understanding. Especially if you are new to functional programming.
Please note that the Idris book was written for Idris1, we are using Idris2.
For differences between the book and Idris2 please see:
Generally speaking, the Idris book covers core functionality in programming with dependent types.