Idris version of the languages presented in "Types and Programming Languages"

https://www.cis.upenn.edu/~bcpierce/tapl/

Uses Idris 2, version 0.3.0-f1085b98a. To run a file, use

idris2 -p contrib -p sop -p elab-util Main.idr

in the file you're interested in. You need to have sop and elab-util installed first.