[Agda] Working with coinductive trees?

[Brandon Moore]

> From: Nils Anders Danielsson <nad at chalmers.se>
>On 2012-02-24 16:11, Brandon Moore wrote:
>> There's a bit of difficulty in Coq as unfolding terms has to
>> be done by applying an equality, but it's mostly straightforward.
>
>The lemma clo in your development relies on a feature of Coq which
>breaks subject reduction.
>
>> This seems to be rooted in generativity - it takes a bit of trouble
>> with a with-clause to match on a delayed subterm, and even after doing
>> so the results can't be recorded in the context by refining the
>> subtree to look like (# pat).
>
>Generativity is indeed annoying. You could try to avoid mentioning ♯_
>unless absolutely possible. The attached development uses conditional
>coinduction to accomplish this.

Thanks. That's a nice technique, and so far it avoids all the difficulties I
was having.

Brandon