Had a somewhat informational meeting with Frank. All the little details of the Twelf codebase are still gradually making more sense. Much remains for me to understand on the metalogic side of things, but maybe I'll get around to studying it harder-core eventually.
Went to Joe Mama's after-11 half-price with
combinator, pete, and dan blandford. Got the penne and sausage and actually mostly finished it this time.Got a lot of hacking on Twelf done in the afternoon and after dinner. As of 3:00am, The "canonically weird" irrelevance unification problem
Ex Y . [x/a] c * x =? [x/a] Y
finally is solved correctly by my hacked copy
of Twelf, modulo the uninstantiated new evar
being left as a "dangling deBruijn index". I
should easily be able to fix that, though.
