[Agda] Coinductive families

[Nils Anders Danielsson]

On 2010-10-06 13:40, Thorsten Altenkirch wrote:
> This would be strange. There are structures which clearly have a
> record flavour and which show up in the middle of a mutual recursive
> definition and then I am not allowed to use records? There is also the
> potential discontinuity: you are start with a non-recursive structure
> and then make it recursive and now you have to rewrite all your code?

I doubt that you need to rewrite all your code, unless all your code
depends on η-equality (or if the change you performed affects all code).

> I think it should be clear that eta expansion stops at recursive use
> of types. In PiSigma this is very clear due to the use of rec.
> Something like this may also work for Agda.

ΠΣ doesn't have η-equality. I interpret your statement as follows:
Records should only be allowed to be recursive if the recursive
occurrences are suitably guarded. (I believe you and I have discussed
this before.) This might work, at the cost of another syntactic check.
However, I don't want to allow /unrestricted/ recursive records.

--
/NAD