Materials for my Haskell eXchange 2015 talk, including the slides.

See formal-logic for more formalisations.

To check all files automatically:

$ make

To load a particular file for interactive use:

$ agda --safe -I -i src src/FILE.agda

$ ghci -Wall -isrc src/FILE.hs

$ idris -i src src/FILE.idr

Tested with Agda 2.4.2.3, Idris 0.9.19, and GHC 7.8.4.

Made by Miëtek Bak. Published under the MIT X11 license.