「Coqの型クラスの使い方：バンドル方式とアンバンドル方式」で紹介したスピターズ／ファンデル・ウィーゲンのアンバンドル方式の実例をモノイド以外にもうひとつ。半環（semiring）をやってみます。"Type Classes for Mathematics in Type Theory"にある例…

「Coqで定理を記述してみる、型クラスとか使って」に次のような断り書きを入れました。 ミート半束のような代数構造をどう定義するのが良いのか、あんまり分かってないのですが、まーまー使える方法を紹介します。この方法には課題があることを注意しておき…

Coqの証明スキルが全然身につきません。ダメです。それで、証明はともかくとして、定理の記述方法を試行錯誤してました。短くて抽象度が高くて読みやすい記述はどんなものだろう？ と。型クラスを使うのがよろしいようです。内容： 例題：ミート半束と順序集…