[Agda] Handling the Impossible

[Ulf Norell]

On Fri, May 9, 2008 at 7:31 PM, Lennart Augustsson <lennart at augustsson.net>
wrote:

> Why is there a special pattern?  Wouldn't _ or a variable work?


In order to be allowed to omit the right hand side you need to ask the type
checker's permission. () is how you do that. Absurd patterns also makes the
program easier to read. In principle the type checker could search all the
variables and wild cards for empty types when you omit the right hand side,
but in this case it doesn't cost anything for the programmer to explain
what's going on and save the type checker and the reader of the program some
work.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080509/3c588fa9/attachment.html