Epilogue

The purpose of this page is to ensure that there’s always something to be busy with. I’ll try to keep this page up to date with tasks that are both necessary and possible.

11 September 2006

• Core Theory
  • replace tipped-list treatment of tuples with pair-and-void done!
  • implement an inductive-recursive universe (as a step on the way to a container-based treatment)
  • re-implement observational equality
  • shift the Checking monad to something more informative about failure
  • sync the design doc, the implementation and the EpiTome never done!
• Ecce
  • tidy the modules; at the moment it’s all a lump called EcceThump done!
  • ensure that we have a command-line version we can makily make done!
  • implement better navigation for proof state
  • implement definition aliasing
  • implement some sort of save and load
  • implement type constructions with Π-parameters
  • implement gui for proof state
  • permit deletion of top layer definition
  • fix bug in deletion: if the mother dies, her children die too
• Miscellaneous
  • make Epilogue offer reasonably up-to-date pdfs of the design document and the EpiTome
  • feed Edwin’s compiler from the Ecce state