Twitterでつぶやいていた内容の一部をメモにしておこう。無名指標と入れ子指標無名指標または指標リテラルは、sig {...} の形で書く。 sig { sort U operation e:ε → U operation m:(U, U) → U }これはモノイド指標（monoidal signature、「モノイドの指標」…

"Canonical Structures for the working Coq user" by Assia Mahboubi, Enrico Tassi （https://hal.inria.fr/hal-00816703v1/document）の最初の段落： One of the key ingredients to the concision, and intelligibility, of a mathematical text is the …