[Agda] Codata and "with" matching

[Nils Anders Danielsson]

On Wed, Sep 3, 2008 at 03:57, Shin-Cheng Mu <scm at iis.sinica.edu.tw> wrote:
>
> On Sep 3, 2008, at 2:35 AM, Nils Anders Danielsson wrote:
>>
>> 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.
>
> Hmm... I am still confused, but I guess your hint has something
> to do with putting the with expression in the right context.

Contrary to its name there is nothing magic about "magic with". If the
goal type is P[e] and you do "with e", then the goal type turns into
P[x] where x is a variable which you can pattern match on in the with
clause. Occurrences of e in the context are also replaced with x.
(There is more to be said about with. See Ulf's thesis, for instance.)

If e does not occur in the goal type, then the goal type does not
change.

> Is it a rule now that all local definitions in a (co)recursively
> defined function must be (co)recursively defined as well?

Local definitions are always mutually defined with the top-level one
(but not necessarily with each other), and currently all definitions
in a mutual block need to be of the same kind (recursive or
corecursive).

Following Lennart's suggestion to find and make use of strongly
connected components in the call graph would alleviate this problem.

-- 
/NAD