Coqの起動のしかた

ターミナルでcoqtopと入力すると対話型証明支援系Coqが立ち上がる。
さあ、今日からCoqを使ってみよう!

/yoshihiro$ coqtop
Welcome to Coq 8.0pl3 (Jan 2006)

Coq <

CoqではCoqコマンドというものを使って操作をおこなう。
まず最初にCoqを終了するCoqコマンドを使ってみよう。

文法 [Quit.]

Coqコマンドは必ず大文字で始まり、最後にはドットがあることを忘れないようにしよう。

Coq < Quit.
/yoshihiro$