関数型ガール
え～、あれをナニしたりしたものです。もとネタわからない人はこちらへ。
謝辞
まず最初に、Pierce先生、結城先生ごめんなさい。出来心で書いてしまいました。シャレだと思ってご勘弁ください。
目的
最初にSoftwareFoundationに触れた時感じた驚きは、「これは何だか教材として新しい！」というものでした。
実際にSoftwareFouncationの.vファイルを開いて読み進めてもらうと分かると思いますが、この教材は完全にプログラムのソースファイルと読み物が一体化していて、コメントを読みながら１行ずつ実行し、その結果を目で確認しながら学習を進められます。
まるでCoq自体がチュートリアルシステムを成しているかのような動きをするのです。
そして、自分自身でそのソースファイルを編集しながら実行を続けられ、エラーがあれば少し前まで戻って修正して再度実行、というサイクルをファイルを開いたまま続けられます。
これは画期的なことではないかと思うのです。
実際にSoftwareFouncationの.vファイルを開いて読み進めてもらうと分かると思いますが、この教材は完全にプログラムのソースファイルと読み物が一体化していて、コメントを読みながら１行ずつ実行し、その結果を目で確認しながら学習を進められます。
まるでCoq自体がチュートリアルシステムを成しているかのような動きをするのです。
そして、自分自身でそのソースファイルを編集しながら実行を続けられ、エラーがあれば少し前まで戻って修正して再度実行、というサイクルをファイルを開いたまま続けられます。
これは画期的なことではないかと思うのです。
この「関数型ガール」は、そういったCoqチュートリアルのデモのようなものだと思ってください。CoqIdeかemacs+ProofGeneralで.vファイルを開き、コメントを読みながらラムダさんの言葉に従って手を動かしてください。なんとなくこの意味が分かってくると思います。
注意など
CoqIdeは、環境によっては日本語をうまく扱えない場合があります。少々面倒かもしれませんが、emacs+ProofGeneralをお勧めします。
内容は、SoftwareFoundationsのBasics.vの一部を抜き出してコメントを差し替えただけです。ある意味「超超訳」と言えなくないかもしれません（言いすぎ）。
内容は、SoftwareFoundationsのBasics.vの一部を抜き出してコメントを差し替えただけです。ある意味「超超訳」と言えなくないかもしれません（言いすぎ）。
本文（html）
関数型ガール
HTMLでも読めるのですが、できれば下の.vファイルをCoqIdeかemacs+ProofGeneralにかけてください。真意はそちらのほうが伝わります。
HTMLでも読めるのですが、できれば下の.vファイルをCoqIdeかemacs+ProofGeneralにかけてください。真意はそちらのほうが伝わります。
ファイル
ご意見、ご要望はTwitterのほうへ @katayama_k
今日： - 人
昨日： - 人
トータル： - 人
昨日： - 人
トータル： - 人
