「Certified Programming with Dependent Types関係」の編集履歴（バックアップ）一覧はこちら
追加された行は緑色になります。
削除された行は赤色になります。
*Certified Programming with Dependent Types (CPDT)を読む為の前提
この教科書は、オリジナルなtacticのcrushというのを導入して、色々自動証明をさせています。なので、crush出来る様にしておかないと、教科書の証明を写経できません。crushを使う方法ですが、
-Coqをインストールしておくのは当然。
-CPDTの付属ファイルを入手する。詳しくはCPDT 1.6章を読むべきだが
-- http://adam.chlipala.net/cpdt/cpdt.tgz をダウンロードする。
-- 適当なディレクトリ (~/cpdt/とか)で展開し、makeする。
-- Coq起動時に、coqtop -I ~/cpdt/src とオプションでソースディレクトリを指定。
-- Coq内で、Require Import Tactic. と Tactic.v を読み込んでおく。
-- こうすると、crushというtacticが使用出来る。
*Certified Programming with Dependent Types (CPDT)を読む為の前提
この教科書は、オリジナルなtacticのcrushというのを導入して、色々自動証明をさせています。なので、crush出来る様にしておかないと、教科書の証明を写経できません。crushを使う方法ですが、
-Coqをインストールしておくのは当然。
-CPDTの付属ファイルを入手する。詳しくはCPDT 1.6章を読むべきだが
-- http://adam.chlipala.net/cpdt/cpdt.tgz をダウンロードする。
-- 適当なディレクトリ (~/cpdt/とか)で展開し、makeする。
-- Coq起動時に、coqtop -I ~/cpdt/src とオプションでソースディレクトリを指定。
-- Coq内で、Require Import Tactics. と Tactics.v を読み込んでおく。
-- こうすると、crushというtacticが使用出来る。
