[Agda] pattern matching syntax in records

[Chris Casinghino]

Hi Agda hackers,

I'm having trouble defining a record field in ways that will let me
pattern match.  I keep getting syntax errors.  As an example, we might
define the record type:

record predator : Set₁ where
  field
    prd : ℕ -> ℕ

However if I try to fill in prd this way:

r : predator
r = record
  { prd zero = zero
    prd (suc n) = n }

I get the syntax error:

  Parse error zero<ERROR> = zero prd (suc n) = n } ...

And if I try to fill it in with a where clause:

r : predator
r = record
  { prd = foo
      where
        foo : ℕ -> ℕ
        foo zero = zero
        foo (suc n) = n }

I get the syntax error:

  Parse error where<ERROR> foo : ℕ -> ℕ ...

Of course, in this case I could define prd separately, but for
examples deep in a dependent record this could be very inconvenient
(as it is in what I'm working on).

Is there a syntax to do this?  I couldn't find any notes on the wiki
or mailing list archives.  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.

Thanks for your help!

--Chris