[Agda] Pattern matching on irrelevant data

[Nicolas Pouillard]

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 :)

> On 04.10.11 10:35 AM, Nicolas Pouillard wrote:
>>
>> On Tue, Oct 4, 2011 at 10:20 AM, Andreas Abel<andreas.abel at ifi.lmu.de>
>>  wrote:
>>>
>>> On 03.10.11 10:51 PM, Dan Doel wrote:
>>
>> [...]
>>>
>>> 3. As you pointed out with your refl-example, irrelevant matching against
>>> a
>>> data type with just one constructor does yield new information in some
>>> cases.  This indeed makes my enterprise questionable (the new stuff I
>>> pushed
>>> yesterday).
>>
>> 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?

-- 
Nicolas Pouillard
http://nicolaspouillard.fr