reswatson

My two cents as a user of Idris for writing maths software and for theorem proving: I always get worried when someone says Idris is a practical programming language and...

Using version 0.3.0 All the ipkgs compile using idris2 --build XXXX.ipkg, except lecture2 as already noted. Assuming you are in the right directory. And assuming (unlike me at first, being...