[Agda] Pattern matching on irrelevant data

[Andreas Abel]

On 04.10.11 12:46 PM, Nicolas Pouillard wrote:
> On Tue, Oct 4, 2011 at 12:06 PM, Andreas Abel<andreas.abel at ifi.lmu.de>  wrote:
>> Irrelevant matching against data has been disabled by default now, for
>> experimentation with it there is the option
>>
>>   --experimental-irrelevance
>
> This is better this way :)
>
>>> Let's throw in a naive question... Could we restrict the irrelevant
>>> pattern matching to the cases it does not
>>> add any information? Is it easy to implement? Does this retain some
>>> useful examples?
>>
>> Good questions.
>>
>> To answer the first, I think "terminating" linear pattern families are safe
>> to match on irrelevantly.  That excludes the identity type and also the
>> accessibility predicate.  This might already answer the second question; the
>> interesting examples are gone then.
>
> I fail to see why your div example would be rejected? Would it be?

To show that Div! is terminating we need to show that

   suc n > minus n m.

But if we could check this, we could have checked termination of div in 
the first place.

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
http://www2.tcs.ifi.lmu.de/~abel/