読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

Coqの起動のしかた

Coq入門 Quit

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

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

Coq <

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

文法 [Quit.]

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

Coq < Quit.
/yoshihiro$