[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