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