2012-05-31から1日間の記事一覧

また ill-typed term が出てくる例

証明がうまくいかなくて工夫が必要な事例を集めようとしています。今回のは Coq'Art にも似たような例が書いてあった気がしますが。 問題設定 Z -> Z な関数 f と,Z -> Prop な述語(「よい」整数の定義)が与えられます。 0 書けたら,sum の値は証明の中身…