■

• どれが型で、値で、という区別。
• どれが命題で、証明で、という区別。

慣れるしかないとはいえつらい。

しばしば出て来る数学用語についても、もう少し知っておく必要がある。直積、関係、反射的、推移的、対称的、etc...学がないとつらいね。

SoftwareFoundationsも微妙に変わっているので、勉強がてら翻訳してるけど、Logic.vによく出て来る、"Proof Term"って何て翻訳すればいいんだろ？

https://github.com/moritanon/sfja/