[Agda] mutual strangeness

[Gyesik Lee]

Hi,

>  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.

I would like to make one remark on this.
It seems that the mutual inductive definition in Agda is a bit more
general than in Coq.
As long as I know, in Coq, D_i should not occur in any of T_k.
(it is written so in the most recent version of Coq reference manual
unless I misunderstood it.)

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.
I thought it was the point of Thorsten's question.

Gyesik