[Agda] Irrelevance + instance arguments = inconsistency in 2.3.0

Andreas Abel andreas.abel at ifi.lmu.de
Wed Jan 11 18:25:10 CET 2012

This should be fixed on the darcs version (2.3.1) now.  Can you please 


On 1/11/12 3:40 PM, Andreas Abel wrote:
> Hello Adam,
> Thanks for filing the report!
> On 1/11/12 1:17 PM, Adam Gundry wrote:
>> I realise that irrelevant record projections are inconsistent anyway
>> [1], but I think I've found another problem with irrelevance that
>> doesn't depend on them and uses instance arguments instead.
> The problem you describe is independent from irrelevant record
> projections, since you do not use any.
> Instance search does not respect irrelevance, this is why you can derive
> a contradiction. However, that should be easily fixable.
> Cheers,
> Andreas

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de

More information about the Agda mailing list