[Agda] mutual strangeness

[Nils Anders Danielsson]

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.