[Agda] Instance fields

[Nils Anders Danielsson]

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

-- 
/NAD