[Agda] Pattern matching on irrelevant data

[Nicolas Pouillard]

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?

-- 
Nicolas Pouillard
http://nicolaspouillard.fr