Coq/SSReflect/MathComp Tutorial
定理証明支援系Coq/SSReflect/MathComp入門
- 資料:
- slides (last version):
- slides (previous versions):
- : 京都大学の集中講義で使った資料(約14時間): slides (addendum about groups)
- : 名古屋大学の集中講義 で使った資料(約9時間): slides (addendum about groups)
- : 日本ソフトウェア科学会 第31回大会のチュートリアル (定理証明支援系Coq入門) で使った資料(4時間): slides
- Coq/SSReflect/MathCompの設定
- 参考文献:
- 追加資料:
- Coq/SSReflectファイル (line-by-line実行のため) (xmlファイルはproviolaによる):
- logic_example.v (html, movie)
- ssrnat_example.v (html, movie)
- predicative_example.v (html, movie)
- dependent_example.v (html, movie)
- ssrbool_example.v (html, movie)
- tactics_example.v (html, movie)
- view_example.v (html, movie)
- eqtype_example.v (html, movie)
- fintype_example.v (html, movie)
- tuple_example.v (html, movie)
- implicit_example.v (html, movie)
- mybigop_example.v (html, movie)
- bigop_example.v (html, movie)
- finset_example.v (html, movie)
- bigop2_example.v (html, movie)
- group_example.v (html, movie)
- permutation_example.v (html, movie)
- matrix_example.v (html, movie)