[Agda] emptiness checking with strings

[Ulf Norell]

On Jan 31, 2008 2:09 AM, Dan Licata <drl at cs.cmu.edu> wrote:

> Hi everyone,
>
> Given the usual equality type Id M N and the empty type Void, I'd like
> to write a function
>
> contra : Id "nat" "exp" -> Void
> contra ()
>
> However, the emptiness checker doesn't notice that this type is
> uninhabited (like it would if "nat" and "exp" were two different
> constructors of a datatype).
>
> Does anyone know a workaround?  Also, would it be hard to catch this
> case (i.e., treat string literals as constructors), or is this just a
> feature that's not implemented yet?


It wouldn't be hard at all. In fact a patch has just been pushed that fixes
the issue.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20080131/499bc451/attachment.html