Type-Driven Development - Exercises To run Idris2 inside the project: $ rlwrap idris2 --find-ipkg To load a particular module: > :l "path/to/file.idr"