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 afind-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.