[Agda] Agda with excluded middle is inconsistent

[Thorsten Altenkirch]

On 8 Jan 2010, at 02:58, Nils Anders Danielsson wrote:

> On 2010-01-07 11:30, Thorsten Altenkirch wrote:
>> congratulations! I didn't know about this problem and I think it is a
>> serious issue indeed.
> 
> I agree.
> 
>> Maybe it is a known issue? Nisse? Ulf?
> 
> I don't think so, but there was some scepticism when injectivity of type
> constructors was introduced. See the following thread:
> 
> heterogeneous equality
> https://lists.chalmers.se/pipermail/agda/2008/000153.html

I missed this thread. Interesting, especially Conor's comments.

> I wanted to see how often I have used this feature, so I reverted the
> change Ulf mentions in that thread. It turned out that I only had to
> modify two functions to make the 168 files of the standard library type
> check.

This is good news.

> If reverting this change really is all that is needed to remove
> automatic type constructor injectivity (Ulf?), then I suggest that we
> make this feature optional, or remove it entirely.

I'd be in favour to pragmafy it.

Cheers,
Thorsten
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100108/d71d5e69/attachment-0001.html