[Agda] Coinductive families

[Nils Anders Danielsson]

On 2010-10-05 15:59, Dan Licata wrote:
> Perhaps someone could review for me why you want to treat
> them differently for definitional equality, like Agda currently does.
> For example: does something go wrong if you identify records with
> one-branch datatypes.  I.e. for every one-branch datatype, you
> automatically generate all of the projections and make eta (p = (fst p,
> snd p)) hold definitionally?

Some reasons:

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

* If Agda generated projections automatically, what would they be
   called? All record fields have names.

--
/NAD