[Agda] mutual haskell types with MAlonzo

Perikov Pavel perikov at gmail.com
Sat May 28 16:36:21 CEST 2011


Hi list.

supposing I have the following haskell code: 

data Pat = A | B Exp
data Exp = C | D Pat

The above is perfectly legal haskell. Could I make a wrapper for this types in Agda?
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 #-}

makes the compiler complain about Pat cannot be translated to a haskell type (because translation of Exp is unknown at this point I suppose)



More information about the Agda mailing list