Epilogue

I’ve been doing a bit more work on the Epigram libraries. Check out two new library snapshots:

• Simple overview
• Complete overview

It’s starting to look as messy as a proper library.

In general, every datatype has an associated file with common operations. A separate file contains the proof that equality is decidable for that datatype. As you can see from the more advanced snapshot, there are quite a few files that still need a bit of filling in and a few others that need a bit of cleaning up. I reckon the status of the libraries might be a good agenda point for the next Epigram meeting.

I do have a short wishlist for new Epigram features that would make my life a bit easier:

• Add the ability to include files outside of the current directory. This shouldn’t be too hard, but will probably need to be implemented on the XEmacs side.
• Being able to typecheck a file straight from the command-line. This one is a bit trickier. One feasible option would be getArgs in the Main file, followed by a find-file,blat-epigram and elaboration. Things would be even nicer if we can avoid invoking XEmacs - but I don’t know if we can get away with that the way things are implemented currently.

This entry was posted on Friday, July 8th, 2005 at 9:27 am and is filed under Library. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.