The Little Prover

これは、LISPやSchemeに対する、The Little LisperやThe Little Schemerのような関係にある Coqに対するThe Little Proferらしい。

まだ最初の方しか読めていない。ややこしい。

focusをあてている部分にルールを適用するその仕方を繰り返し説明しているのだけれど、なんだかよくわからない。英語の読解力がないからだろう。

もう少し読み続けてみよう。

 とはいえ、Juliaが優先だと思う。