Epigram Developers' Documentation

Epigram has/will have various bits and pieces, and some of them might be worthy of comment, one of these days:

• Utilities: general handy stuff, like the Idiom library.
• Syntax: syntactic equipment, like the lexer, the grouper, the parsers and the scoper.
• Term: implementing the underlying type theory, and related apparatus.
• Igor: representing and manipulating the proof state.
• Elaborator: translating scoped syntax into the underlying type theory, a bit at a time.
• Editor: what it says, using the syntax tools to make stuff to send to the Elaborator; mediating the responses somehow.
• Interface: hooking the elaborator to an editor, yielding an interactive system.

Epigram's Makefile is not very smart just now. The default target just updates the datestamp module and then calls ghc --make. There's also a ghci target which invokes ghci with the right flags. I'm sure it could all be slicker.

Epilogue