■

よく晴れる。しかし寒い。さすがに12月だ。起床は8時半、出勤して今後のコードのデザインを考える。
夕方、Ktさんが新しく書いたインストールマニュアルのテストも兼ねて、Agda2を最新版に更新する。前にインストールした版は10月後半のもので、Terminationの判定などに関してだいぶ進歩したという話だ。もしかしたら、前の版でterminateしなかった知識様相論理のsatisfactionも、今度の進歩した版ではterminateしてくれるのではないかと淡い期待を抱いていた。インストール中にGHCをkillしてしまい（ちなみにAgda2のインストーラーはHaskellで動いている）最初からやり直しというアホな一幕もあったが、19時半にやっとインストール終了。いざ新バージョンを動かしてみると・・・Satisfactionの定義で「以下のケースの定義がありません」と、前回指摘しなかった問題点をゾロゾロと出力してきた・・・問題が増えた。
20時に退所、21時半に阪急駅に着くも、市バスが満員で乗れず、寒い中歩いて帰る。夕食はミートソース。