Jason (jcreed) wrote,

Dreams: one, involving believing that lars_chan had a great-uncle by the name of David Semesky who was giving me advice on something or other. Two: good ol'-fashioned flying dream. I love flying dreams.

Woke up, and worked out, at last, I think, how to do the translation from LF to LF*. At first I thought that I'd have to actually define a function whose domain was typing derivations, yecch. I hate trying to work out the syntax of that, involving huge \left(s and \right)s around prooftree environments. Fortunately, I think I know how to avoid that now, though my first attempt got pretty far before I realized I needed more type information around, and that doomed that.

Man, dependent type theories are like rampantly incestual families, I tell you. Terms gettin' with types, types gettin' with terms... A fella cain't hardly sort it all out.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded