Jason (jcreed) wrote,
Jason
jcreed

Realized due to the possibility of substituting c- constants for variables in synthesizing positions, I need to carry full dependent types with substitutions. ARG ARG ARG. That invalidates a LOT of recent work.

Went to KGB for a little while. I notice my attention span for it is steadily decreasing. Skipped out after a half hour for piano time. Oh man. So good. My fingers were in rare shape, somehow doing exactly my brain's bidding quite well. I was practically in a trance-like state playing latin-y stuff over Am-E7-E7-Am and later a minimalist F7-G7 pattern. Oh man. The fact that the piano was horribly out of tune didn't even bother me. Such a good time.

Tomczack and Andreas came by to an ad-hoc office hour at 6:30. I think I was at least a little helpful. Klaus is tossing an ungodly amount of group theory at the kids.
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 

  • 1 comment