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.