Coqの起動のしかた
ターミナルでcoqtopと入力すると対話型証明支援系Coqが立ち上がる。
さあ、今日からCoqを使ってみよう!
/yoshihiro$ coqtop Welcome to Coq 8.0pl3 (Jan 2006)
Coq <
CoqではCoqコマンドというものを使って操作をおこなう。
まず最初にCoqを終了するCoqコマンドを使ってみよう。
文法 [Quit.]
Coqコマンドは必ず大文字で始まり、最後にはドットがあることを忘れないようにしよう。
Coq < Quit.
/yoshihiro$