[Agda] mutual haskell types with MAlonzo

[Andreas Abel]

Hi Perikov,

it seems like Agda does not support mutual COMPILED_DATA pragmas.  I 
looked at the code of the type checker and it handles them individually 
instead of in a bundle.  So mutual types are not supported.

I file a bug report.

Cheers,
Andreas

On 28.05.11 4:36 PM, Perikov Pavel wrote:
> mutual
> 	data Pat : Set where
> 		A : Pat
> 		B : Exp ->  Pat
> 	data Exp : Set where
> 		C : Exp
> 		D : Pat ->  Exp
>
> {-# COMPILED_DATA Pat  Pat A B #-}
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/