A work-in-progress proof of the pacman-completeness of Idris. Requires: git@github.com:steshaw/idris-sdl2.git