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.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded