2008-03-08から1日間の記事一覧

Coqで、クイックソート

(* 注意:今回はCoq 8.1以上を使用。 *)今回は、らくがきえんじんで、昔 言及されていた、クイックソートに挑戦してみる。Coqで、再帰する関数を書く場合は、Definitionコマンドではなく、Fixpointコマンドを使う。 しかし、Fixpointによる関数定義では…