[Agda] Re: Do we really want special case casts?

[Nils Anders Danielsson]

On 2009-10-19 19:38, Samuel Gélineau wrote:
> Thanks, but that page is explaining why the top-to-bottom ordering of
> the patterns matters, isn't it?

Maybe the explanation is not as explicit as it should be. The key point
is that it should always be possible to compile Agda's pattern matching
down to well-typed case trees (where every case does pattern matching on
a single variable, and every pattern consists of a single constructor
applied to variables).

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.