Jason (jcreed) wrote,
Jason
jcreed

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.
Tags: twelf, work
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 0 comments