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

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