Jason (jcreed) wrote,

...make lemma-nade.

Haha! Take that, you lousy mutter-mutter lemma!

I think I've proven it, now. It required tweaking the typechecking algorithm. I was sitting in Sam's alternating between trying to find a counterexample, trying to prove it, and taking bites of the sandwich. I paused for bit to think about soundness, and realized that for it I only needed the types of an irrelevant function and its argument to match up in the promoted context, because I can type-convert to the `good' type in that context, and then fall back down into the irrelevant typing judgment. So I tried proving completeness for the weaker assumption that the types are equal in the stronger context (whee, contravariance) and succeeded! Assuming I didn't fuck anything up, anyway. I should ask Frank to proofread my, uh proof, probably.

  • (no subject)

    Guy from Seattle team we've been working with showed up today at work; no matter how much I'm generally comfortable working with remote teams (and I…

  • (no subject)

    Sean's back in town --- good fun working with nonremote teammates.

  • (no subject)

    Played some board games at the fb office with newly-arrived-to-nyc dan blandford and some friends-of-friends of his. Codenames and…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded