「WindowsへのCoqのインストール」： 事情があって、AgdaかCoqを触ってみようか、と。 事情というのは、個々の命題の証明（確認）は割と簡単そうだが、命題がイッパイあるのでウンザリな状況のことです。家計簿の計算が筆算だと面倒だから電卓を使いたい、という状況と同様です。 それでCoqのインストールは済んだのですが、処理系の使い方が分からない。個々の操作は覚えていけばいいのでしょうが、そもそもCoq処理系が何をするものなのか？ が理解できないのです。Web上にCoqの解説は幾つもあるのですが、「いやいや、そうじゃなくて、それ以前のことがサッパリわからんのですけど」という感じ。スタートラインに立てない。 それで、「Coqの解説」じゃなくて「Coqの仕様」を読んだほうがいいのかも、と https://coq.inria.fr/distrib/current/refman/ （リファレンス
