Coqの構文について思うことをメモしていく。 letが1個の変数しか束縛できないことは意外と不便ではない。ブロック囲み記号（特にエンドマーカー）が不要なので入れ子が深くならない。単に代入文を並べている感じになる。 matchのケースの先頭に余分な '|' を…

Coqの型クラスについて思うことをメモしていく。 フィールド名が大域的なのは最低。フィールド名を局所化すれば出来る事が色々あるのに。ミクシンはその一例。 フィールドアクセッサの構文がない。f x の代わりに x.(f) が使えるようだが使いにくいし、そも…

Title: Morita equivalence of many-sorted algebraic theories Authors: Jiˇrí Adámek, Manuela Sobral, , Lurdes Sousa URL: https://estudogeral.sib.uc.pt/bitstream/10316/4616/1/filee8df8c9585d34e1a8d56fdaf0460d008.pdf によると、森田同値は2つの…