Author here. Glad to see so many people interested.

I think people will find this useful as an example is programming in Idris. While there are many other resources around, this fills a niche as a fairly complete, self contained program.

Since I wrote it, I've noticed that my programming style is not very standard, especially my approach to proofs, so I'm still working on it.