[Agda] Instance fields

[Martin Stone Davis]

I've found record constructor instances to be useful. My question here 
is whether `field instance foo` or `field instance {{foo}}` should ever 
to be preferred over `field {{foo}}`.


On 08/22/2017 04:14 AM, Nils Anders Danielsson wrote:
> On 2017-08-01 20:42, Martin Stone Davis wrote:
>> Is it *ever* what you want? I haven't yet found a use case where I
>> didn't instead prefer `{{...}}`.
>
> The builtin unit type is defined in the following way:
>
>   record ⊤ : Set where
>     instance constructor tt
>
> However, if there are only a tiny number of examples like this, then it
> is perhaps better to remove this feature (to avoid confusion and
> mistakes), and instead provide the instance above manually:
>
>   instance
>     tt-instance : ⊤
>     tt-instance = tt
>