HiAgda doesn't permit \lambda as a type constructor! I wanted to define a type "lambda-terms" and chose Agda because it supports Unicode. -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.chalmers.se/pipermail/agda/attachments/20160304/90b0f099/attachment.html