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

[kahl at cas.mcmaster.ca]

 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₂
 > 
 > gets translated into
 > 
 >   record R : Set where
 >     field
 >       f₁ : let open M in T₁
 >       f₂ : let open M in T₂,
 > 
 > and you can't use open public in let expressions. I suppose the
 > workaround I described above could be part of the translation, though.

Now much clearer --- thank you very much!


Wolfram