[Agda] Record types are not allowed in mutual blocks

Thorsten Altenkirch txa at Cs.Nott.AC.UK
Fri Mar 18 18:15:58 CET 2011


For what I try to do in the moment it is extremely annoying that I cannot define mutually recursive records. 

Yes, I can emulate this with one constructor data types but I would really like to use fields and field selection directly. 

Is there any way to switch off this check which stops me from doing this?

Cheers,
Thorsten



More information about the Agda mailing list