[Agda] Not implemented: coinductive constructor in the scope of a let-bound variable

[Nils Anders Danielsson]

On 2010-12-29 16:05, Thorsten Altenkirch wrote:
> This is a bit annoying and I don't understand why it isn't
> implemented. Sure there is an easy workaround by just
> lambda-abtsracting instead.

This issue was also documented in the message I just mentioned in
another thread:

   Changes to coinduction
   http://article.gmane.org/gmane.comp.lang.agda/763/

If you want to fix the problem you can start by searching for the string
"coinductive constructor in the scope of a let-bound variable" in the
sources.

-- 
/NAD