Coq 的安装及使用

下载及安装

• 下载地址：https://coq.inria.fr/download

Windows 环境下，安装 coq-8.9.1-installer-windows-x86_64.exe 即可。安装完成后可以打开 CoqIde.

一个简单的例子

采用《Software Foundation》中的一个例子。输入下方代码

Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

Definition next_weekday (d:day) : day :=
  match d with
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => monday
  | saturday  => monday
  | sunday    => monday
  end.

Compute (next_weekday friday).
Compute (next_weekday (next_weekday saturday)).
​

将光标置于 Compute (next_weekday friday). 末尾，点击命令 Go to cursor，程序将会运行到光标处，并输出结果。

保存代码

注意要保存为 *.v 文件。

编译代码

保存文件后，选择 Complie->Complie buffer，编译程序。

编译后，生成 *.vo 文件。