[Agda] pattern matching syntax in records

[Nils Anders Danielsson]

On 2009-08-31 20:24, Chris Casinghino wrote:
> Is there a syntax to do this?

No. Declarations (including definitions by pattern matching and where
clauses) are not allowed inside expressions (this includes record
values, lambda abstractions and let expressions).

> If not, why are the expressions one may write in records crippled in
> this way? I note that lambdas work, but even inside a lambda in a
> record, I couldn't get a where clause to parse.

Ulf should know the answer to this question.

-- 
/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.