|
[Dec. 7th, 2005|03:02 pm]
Jason
|
Made a moderately important breakthrough just now, I think; I figured out how to adapt Karl's hackbindery to work not just in the proof of theorem, but in a typing definition in such a way that I can actually then prove a small sandboxish theorem about it. Anyone's guess if I can make this work for the full theorem, but this is a step that I had serious doubts about ever being able to achieve just hours ago. |
|
