[Agda] Codata and "with" matching

[Nils Anders Danielsson]

On Tue, Sep 2, 2008 at 17:55, Shin-Cheng Mu <scm at iis.sinica.edu.tw> wrote:
>
>   However, after performing a "with":
>
>   unfoldˢ-fusion {f = f} {h = h} {g = g} fuse x with f (h x)
>   ... | (i , j) ~ bisim {! !} {! !}
>
>   The types of the holes do not change at all:

[...]

>   Why isn't "with" refining the types?

If the with expression is not mentioned anywhere in the context when
you do with, then with does not have any effect on the types.

-- 
/NAD