LoginSignup
1

More than 5 years have passed since last update.

AffeldtさんのSsreflectチュートリアルのソースをビルドする

Last updated at Posted at 2015-06-27

目的

https://staff.aist.go.jp/reynald.affeldt/ssrcoq/ にある「Coq/SSReflectファイル」を手元で動かす

必要なもの

  • coq-8.4
  • ssreflect-1.5 (1.4でもOK?)

手順

次の内容でMakeというファイルを作る。

Make
-R .
bigop2_example.v
group_example.v
predicative_example.v
bigop_example.v
ssrbool_example.v
dependent_example.v
logic_example.v
ssrnat_example.v
eqtype_example.v
tactics_example.v
finset_example.v
matrix_example.v
tuple_example.v
fintype_example.v
permutation_example.v
view_example.v

次を実行

sh
coq_makefile -f Make -o Makefile

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
1