[Agda] mutual strangeness

[Thorsten Altenkirch]

Hi,

it seems that constructors are not visible in the types of mutually  
defined functions. This is especially strange since one can just  
define an auxilliary function to overcome this restriction.

E.g. having another go at a total syntax of type theory I tried:

> module tt0 where
>
> mutual
>
>   data Con : Set where
>     empty : Con
>     _*_ : (Γ : Con) → Ty Γ → Con
>
>   data Ty : Con → Set where
>
>   data Tms : Con → Con → Set where
>
>   wkSubst : ∀ {Γ} → (σ : Ty Γ) → Tms (Γ * σ) Γ
>   wkSubst {Γ} σ = ?

and the scoper complaints:

> Not in scope:
>   * at /Users/txa/Drafts/setoids/tt0.agda:13,41-42
> when scope checking Γ * σ

However, it is easy to overcome this by

> module tt1 where
>
> mutual
>
>   data Con : Set where
>     empty : Con
>     _*_ : (Γ : Con) → Ty Γ → Con
>
>   data Ty : Con → Set where
>
>   data Tms : Con → Con → Set where
>
>   _**_ : (Γ : Con) → Ty Γ → Con
>   Γ ** σ = Γ * σ
>
>   wkSubst : ∀ {Γ} → (σ : Ty Γ) → Tms (Γ ** σ) Γ
>   wkSubst {Γ} σ = {! !}

which is accepted. Hence, wouldn't it make more sense to get rid of  
this restriction alltogether?

Cheers,
Thorsten
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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090131/ec7ecea0/attachment.html