Idris: Software Foundations PDF
Although no google results ever turned it up, there’s a pdf with a lot of proof related exercises in idris:
This comment on a tragically uninformed post by me on reddit explains the use of the contra argument to DecEq’s No constructor well, as well as introducing the above pdf. Hopefully dropping it on medium will make this stuff more visible.
Also don’t do what I tried to do :-)