Description
萩原、アフェルト 著 「Coq/SSReflect/MathCompによる定理証明」森北出版 の3章を読んでいきます。
- 3.9 コマンド Definition, Lemma ... の Defined の例
- 3.15 コマンド Record, Canonical の magmaの例
- 3.8 〜 3.16
の予定です。前回までの内容については、リンクからたどってください。
参加者は上記の本を持参してください。 SSReflect/Mathcomp をインストールしたPCを用意してください。
インストール方法などについての質問も常に歓迎です。
会場は直前に変更になる場合があります。 参加登録された方も、当日の本ページおよびTwitterの ハッシュタグ #ProofCafe に注意してください。
以上
Feed
2019/09/21 12:21
#ProofCafe Omega に代わる自動タクティク lia など https://coq.inria.fr/refman/addendum/micromega.html
2019/08/31 23:56
#ProofCafe 3.15 Magma の例のファイルを差し替えました。コアーションを併用するようにしました。テキストの説明から外れますが、このほうがMathCompの「型システム」の理解に繋がり易いと考えました。