Idris: Software Foundations PDF

art yerkes
Jul 14, 2018 · 1 min read

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

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch

Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore

Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade

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