[Agda] Dependent Types at Work

[Tristan Wibberley]

On Fri, 2008-03-21 at 14:17 +0000, Tristan Wibberley wrote:
  Some stuff about what he really wants to achieve

I got a response off-list which I think probably educates me on this technique.

-- 
Tristan Wibberley

Any opinion expressed is mine (or else I'm playing devils advocate for
the sake of a good argument). My employer had nothing to do with this
communication.