昨年11月の話の続報。 Agda2のdata typeの型の定義で、以下のようなデータ型 Predを定義しようとすると、「dataの型がSortではないのでParse エラーです」というエラーが出ると言う話を書いた。 Pred 0 = Set Pred n+1 = D ->Pred n ただし D: Set とする。 …

昨日に比べればだいぶ暖かく、晴れ間も見える。風邪を引いたらしく、体調が悪い。 起床は9時半、出勤して会議、また発表原稿の作成と発表練習。20時に退所。夕食は牛筋のトマトソースパスタ。