推荐在Linux或者WSL环境下开发。
你需要安装8.15.2版本的coq，在已安装 opam (一般都有，若没有请参考这里) 的条件下运行以下指令
opam pin add coq 8.15.2
推荐在VSCode下安装 VsCoq Legacy (注意不是 VsCoq) 后进行开发。
clone 本仓库后在项目根目录执行
make depend; make
即可编译相关依赖文件。
我们将先学习 coq 的基本语法和证明技术，再学习如何在 coq 中定义算法和证明算法的正确性，最后自选算法在 coq 中定义和证明其正确性。
coq 基础知识的主要教材是 Coq定理证明器入门，其习题作为平时作业。相关的 .v 文件在 basic 文件夹中。
项目选题可见 project.md。