Notes from a Medium-Sized Island [entries|archive|friends|userinfo]

[ website | My Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

[Dec. 7th, 2005|03:02 pm]
[Tags|, ]

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.