[Agda] pattern matching syntax in records

[Ulf Norell]

On Mon, Aug 31, 2009 at 10:27 PM, Chris Casinghino <
chris.casinghino at gmail.com> wrote:

> > No. Declarations (including definitions by pattern matching and where
> > clauses) are not allowed inside expressions (this includes record
> > values, lambda abstractions and let expressions).
>
> Thanks for clarifying.  I suppose I should have looked up the grammar
> first!  I just assumed let and where clauses were in the same
> syntactic category.
>
> I am curious to hear why this distinction is important, and if it
> could be weakened in this case.


I believe the distinction is mostly there for historical reasons and could
well be lifted.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090903/770fecaa/attachment.html