2009-12-14 x = y型と型アノテーションで4択クイズ Coq 概要 2回ハマったのでメモ。 eqの定義とパターンマッチ(の型アノテーション)の難しさのせいで、 eqがtransitiveであることの証明は意外に難しい。 続きを読む