More Epilib

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

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.

Leave a Reply