Jason (jcreed) wrote,
Jason
jcreed

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.
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 

  • 8 comments