September 20th, 2003

beartato phd

(no subject)

Went to KGB's "get bored, get carded" event, played part of a game of Risk, a little Set, and a very little Mao (thank you very much, isildur). Chatted and wandered around with pumpkinn_king afterwards. Ran into two members of The Girls setting up for a late-night practice in the OSC. Went to Ritter's, got some tasty pancakes. She, ravioli. No pants were stolen, though vague threats thereof were implied. An altogether pleasant evening. I envy her girl-attracting superpowers!
beartato phd

(no subject)

Dream: the late Wesley Willis's house was down the street, so I snuck into it and played his keyboard. After I left the house some woman (surviving relative of his?) berated me for not getting in touch with her earlier, making the assumption that I actually knew him and hadn't just entered the house illegitimately. Woke up.

It's getting cold in the mornings now. Suckity suck. At least it makes a hot shower feel really good. But I need to get around to actually washing my comforter, since it was used as a Flagstaff-hill-movie-blanket. Other laundry ought to be done, too.
beartato phd

(no subject)

Why am I so tired? There is no good reason. Today: ate tasty food at Olive Garden. Watched some futurama. Put off grading. Need to do laundry still.
beartato phd

(no subject)

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.