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

[Nils Anders Danielsson]

On 2009-12-09 19:06, kahl at cas.mcmaster.ca wrote:
> 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.

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

--
/NAD