[Agda] Question about the meaning of 'abstract'

[Nils Anders Danielsson]

On 2012-11-18 01:23, Andreas Abel wrote:
> Here is another one:  Agda does not know about abstract record fields.
>
> record R : Set₁ where
>    constructor c
>    abstract
>      field
>        f : Set
>      g : Set
>      g = f
> open R
>
> -- fields are never abstract
> test : {A : Set} → f (c A) ≡ A
> test = refl
>
> The abstract is only applied to g, not to f.

This looks like a bug. Ulf once wrote that "You already get an error for
trying to make fields abstract":

   http://code.google.com/p/agda/issues/detail?id=580#c6

> My question:  Do you think it is ok that data constructors can be
> abstract but record fields not?

Can you make individual data constructors abstract?

-- 
/NAD