[Agda] mutual strangeness

[Gyesik Lee]

I see. I overlooked something.
I thought it was just about inductive definition.
Thanks for the nice explanation.

Gyesik

On Sun, Feb 1, 2009 at 10:21 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:
> On 2009-02-01 07:32, Gyesik Lee wrote:
>
>>>  D₁ : T₁ = d₁, …, D_n : T_n = d_n.
>>>
>>> Then D_i is in scope in T_(i+1), …, T_n and all the d_j. Any
>>> constructors defined in d_i are in scope in the type signatures of
>>> later constructors in d_i plus in d_(i+1), …, d_n.
>
>> On the other hand, I don't still understand why constructors in mutual
>> definitions get invisible, I mean, after having finished a mutual
>> inductive definition.
>
> Above I assume that all the D_i are marked as being mutually recursive
> (the definitions are allowed to be (co)inductive-recursive). The
> constructors /are/ in scope in the bodies and type signatures of later
> definitions in the given module, outside this mutual block (unless they
> are shadowed).
>
> --
> /NAD
>
>
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses, which could damage your computer system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.
>
>