The Epigram project woke up again today after a period in which several papers were written on or around the subject of programming (in) Epigram.
It’s Conor’s task for the time being to create a programming language for describing how elaboration problems get solved (or suspended) he has applied Hutton’s razor and is developing Haskell combinators that do the stuff. The curious might find information relating to this in their cvs. This will hopefully lead to a very good idea about what the interface between the UI and the elaborator should be, once that is sorted a lot of doors will fly open around here.
Peter is going to look in to the ST monad library to see if he can’t help Conor make navigating the proof state with updates a lot more efficent.