AffeldtさんのSsreflectチュートリアルのソースをビルドする
目的
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
Author And Source
この問題について(AffeldtさんのSsreflectチュートリアルのソースをビルドする), 我々は、より多くの情報をここで見つけました https://qiita.com/yoshihiro503/items/f5a5d6d59e5d844b4779著者帰属：元の著者の情報は、元のURLに含まれています。著作権は原作者に属する。
Content is automatically searched and collected through network algorithms . If there is a violation . Please contact us . We will adjust (correct author information ,or delete content ) as soon as possible .