Agda コードはUTF-8なので、Texでコードの紹介文を作成しようとすると、コードをそのままコピペしたのでは文字化けしてしまう。特に数学記号（例えば）などは、いちいちsjis へ変換するのは大変。 で、MacOSX上で、UTF-8をそのまま使用・変換できる ptex を…

起床は8時、曇り、湿度は高いが風があるときは涼しい。 本日はCは実家に帰り、私は朝から原稿書き。外出もせず、一日、パジャマのまま過ごす。23時に夕食、冷蔵庫の残り物を電子レンジで温め、ビールと一緒につまむ。