[Agda] weird behavior with large records

Chris Casinghino chris.casinghino at gmail.com
Wed Jun 2 17:58:46 CEST 2010


I've attached a file I'm playing with.  It's just a copy of part of
coq's "FSet" library.  When I try to load the file in emacs, agda
thinks for a bit then stops without loading the file or giving an
error.  Can anyone confirm they also see this odd behavior?  I'm
running agda 2.2.6.

The problem seems to be that I've made a large record (I'm trying to
imitate the style of Agda's standard library, though this record is
bigger than those).  If I comment any three lines in the bottom part
of the file, it loads fine.

Also if I make the bottom section (the "specifications") an inner
record, it loads fine.  This is a fine work around for now (thanks,
#agda!), but I thought I should report the strange behavior.

--Chris
-------------- next part --------------
A non-text attachment was scrubbed...
Name: FSets.agda
Type: application/octet-stream
Size: 3153 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100602/13459271/FSets.obj


More information about the Agda mailing list