ソフトウェアの基礎を読む – １

ソフトウェアの基礎の「Basics_J: 関数プログラミングとプログラムの証明」完了しました。
コードはこちら

この章で学んだこと。

• Coqでの関数の定義方法
• Coqでの証明の流れ
• 基本的なタクティックの使い方

次は、「Lists_J: 直積、リスト、オプション」をやります。明日から仕事なのであまりかけそうにない…

Emacs+ProofGeneralの環境構築

ProofGeneralを下記のURLからダウンロードして解凍後、~/.emacs/dに移動する。
URL： http://proofgeneral.inf.ed.ac.uk/download

~/.emacs.d/ProofGeneral/でmakeを実行。エラーが発生した場合は以下の記事が参考になるかも
Emacs24でProofGeneralを立ち上げた時に警告が出た時の対処

makeが完了したら、init.elに以下のEmacsLispプログラムを追加

(load-file (expand-file-name "~/.emacs.d/ProofGeneral/generic/proof-site.el"))

環境構築は以上で終了。

使い方:

C-c C-h       - Help
C-c C-n       - Next Step
C-c C-u       - Undo Srep
C-c C-RET  - Goto Point
C-c C-a C-p - Print
C-c C-a C-c - Check