よく晴れる、初夏の陽気。起床は9時、出勤して論文書き。16時からテレビ会議、Agdaの新機能について。それからKtさんとCoqの話をする。また、帰納的定義のパースエラーの話の続報について教えていただく（実は論文の当初案が正しかった事が判明・・・今から…