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 :-)

An old programmer learning new tricks.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store