2008-05-27から1日間の記事一覧

型システムで推論プログラムを書くようにcoqコードを書き、coqで証明をやってみる

背景 prologサンプルコードをふと書いてみる - ラシウラで書かれたコードのように、普通の(関数型)プログラミングだと戻り値に結果を返すようなコードになるところは、 戻り値となる変数をパラメータの最後に置く その戻り値パラメータが、結果としてどのよ…