禁酒中

元旦に飲んで以来、酒抜き中です。単に、行くべきお店がお休みなだけだけどさ。代わりにお茶と白湯です。まだ、少し鼻水が残っているので、丁度良い。

おかげで、少し血圧が下がったような気がする。あんまり関係ないか。

そろそろプロシンの発表資料書かないといけないので、Agda いじって感を取り戻さないと。まさか、また一番最初? でも、なんか、

＊　Agda って、部分集合を書けない

ってのを発見してしまった。集合を { x | P(x) } みたいに書いてやれば、P(x) → Q(x) で部分集合になるらしい。でも、それって、Agda の集合とは違う。まぁ、いろいろ面白い。