The Coq mailing list

[Conor McBride <ctm AT cs.nott.ac.uk>]

roconnor AT theorem.ca
 wrote:

> Welcome to the nightmare that is programming with dependent types. ;-)

Would you care to clarify, refine or qualify this remark?

Conor