現在、Agda2で某論理体系を実装中、本日からタイプチェックを始めた。論理体系なので、列計算を定義したいと考えるのは自然な考えでしょう。というわけで、命題の列を定義しようとしたのだが・・・ Agdaのベースとなる直観主義的タイプ理論では、Proposition…

雨。気温が高く、湿度も高い。 起床は8時15分。とても眠い。出勤してコード書き。本日から実装に入るが、直観主義タイプ理論の型の厳しさに泣く（KTさん、ありがとうございます）。いろいろで遅くなり、21時まで残る。22時半に帰宅、夕食はキャベツのオリー…