More than 5 years have passed since last update.
@yoshihiro503in👁 Image
株式会社proof ninja
株式会社proof ninja
AffeldtさんのSsreflectチュートリアルのソースをビルドする
2
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
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme