[Agda] Problem with ``open'' in ``record'' before ``field''

[Nicolas Pouillard]

Excerpts from kahl's message of Wed Dec 09 21:42:05 UTC 2009:
>  Nils Anders Danielsson <nad at Cs.Nott.AC.UK> answered my question:
>  > > If there is another ``field'' after the ``open'',
>  > > I get a ``Not a valid let declaration when scope checking'' message.
>  > 
>  > You can work around this by using open without public before the fields,
>  > and then open public at the very end of the record module.
> 
> This saves a lot of boilerplate!
> 
>  > > Again, I can work around this, but it is tedious ---
>  > > is this restriction intentional?
>  > 
>  > The declaration
>  > 
>  >   record R : Set where
>  >     open M
>  >     field
>  >       f₁ : T₁
>  >       f₂ : T₂

I've just understood that we can split the field sections as well.

Using this pattern:

record R : Set where
  open M
  field
    f₁ : T₁
  open F f₁
  field
    f₂ : T₂

I've nicely cleaned up some definitions, thanks!

-- 
Nicolas Pouillard
http://nicolaspouillard.fr