Jason (jcreed) wrote,

I was going to go to Finding Nemo with tom and ellen but the fact that I had already seen it made it kind of hard to work up any motivation to actually leave the house.

Had a useful idea about this encoding while lying (laying? I can never remember.) in bed. I think I can throw this whole business of a limit predicate on terms out the window and just make the type-level definition
%abbrev lim = [n':nat] {n:nat} {y:phd} ({cvt:phd->hd} token n (cvt y)) -> ge n n' -> hd
and talk about terms at type lim n' for n' cranking down inductively as one chews through S while showing M . S = M' . S implies M = M'. Yeah, I think that should work.

  • (no subject)

    K got back tonight, pretty late in subjective time (3-4am or so, coming from europe) but all in one piece. None of her houseplants, which were…

  • (no subject)

    K is off tonight to Old Country for a couple weeks, to fulfill family-seeing obligations. Sad! Thankfully we still have internet and skype and…

  • (no subject)

    Finally home. This time instead of mysteriously attracting screaming babies I mysteriously attracted full grown adults biting their nails or maybe…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded