DoctorKey 的博客

下载及安装

• 下载地址：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文件。