[Agda] Coinductive families

[Nils Anders Danielsson]

On 2010-10-06 10:04, Andreas Abel wrote:
>
> On Oct 5, 2010, at 5:25 PM, Nils Anders Danielsson wrote:
>>
>> * Using different kinds of definitional equality for one- and
>> two-constructor data types (or recursive and non-recursive
>> one-constructor data types) may be confusing. By using "record" you
>> explicitly ask for η-equality.
>
> But this would not require a completely different syntax.

No, but I like using the "field" notation for things with many fields.

-- 
/NAD