2008-06-04 code-sprint 四日目 Agda 論文の続き。昼食は昼食は大学のカフェテリアで魚料理。食事中、D先生にMatin-Lofの '71年論文で循環性()がその中核テーマだったので驚いた、と言った話をすると、テーブルの向こうにいたC先生がいきなり身を乗り出して来たので驚く。学者だ。C先生からHurkensのパラドックスのコピーをいただく。 本日は wiki reference manual の某項目の最初を書く。A氏に見てもらって、いろいろな例を提供してもらい、18時まで加筆を加えた。