いよいよ本題の定理証明へ。 3.2 Lemma hoge : … で証明すべき式を宣言。hogeは式につけられる名前。証明が完了すれば以後定理としてhogeの名前で参照できるようになる(らしい)。 Propは命題、/\は論理積を表してる。ということで論理積演算で交換律が成り立…

2.1 定数の定義 Definitionで定数定義というかbindですね。関数をbindするには下の略記が使えると。 2.2 条件式 ブール値を扱うにはBoolをImportしておく。 あるデータ型に対してどんな関数が定義されているかは、SearchやSearchAboutで調べられる。 2.3 自…

Checkは定義を表示。 Eval compute in ex でexを評価 という解釈でいいのかな。

定理証明器のひとつ、Coqをちょっといじってみようかと思い立ったので、この辺を参考にして、とりあえずCoq in a Hurryを写経してみようかと。

読んだ本の数：7冊 読んだページ数：1449ページストーリー・セラーメタ構造だったり、全体的に重い色調だったりで、有川作品としては異色作と言えるのではないかと。でも、描かれる夫婦の関係はやっぱりベタ甘読了日：09月01日 著者：有川 浩図書館戦争LOVE&…