OLEG, A Type Theory With Holes, Lets And Guesses
You Can't Put A Hole Where A Hole Don't Belong
These slides describe the method I used for adding a sound account
of holes (less informatively known as metavariables) to an existing
dependent type theory, without using a notion of explicit substitution.
I don't claim it's the best way of doing things, just that it's very
cheap, and required only a small rearrangement of LEGO.
Since the slides tend to be animated or multistage, each `episode'
is represented by an HTML frameset, with the images on the left
and the navigational information on the right. Simply clicking on
each link in turn through the body of the commentary will operate
the correct sequence.
So, here's the place to begin
Conor's home page.