SUHARA Hiromichi wrote a comment.

2019/09/21 12:27

#ProofCafe 加減積と不等号を MathComp の定義から バニラCoqの定義に書き換えるという意味では、前前前回紹介した内容と同じです。

SUHARA Hiromichi wrote a comment.

2019/09/21 12:23

#ProofCafe lia を MathComp から使えるようにする https://github.com/amahboubi/lia4mathcomp

SUHARA Hiromichi wrote a comment.

2019/09/21 12:21

#ProofCafe Omega に代わる自動タクティク lia など https://coq.inria.fr/refman/addendum/micromega.html

SUHARA Hiromichi wrote a comment.

2019/09/16 16:07

#ProofCafe 第3章演習問題の追加問題をおきました。

SUHARA Hiromichi wrote a comment.

2019/08/31 23:56

#ProofCafe 3.15 Magma の例のファイルを差し替えました。コアーションを併用するようにしました。テキストの説明から外れますが、このほうがMathCompの「型システム」の理解に繋がり易いと考えました。