2016-05-03 The Little Prover 証明系 これは、LISPやSchemeに対する、The Little LisperやThe Little Schemerのような関係にある Coqに対するThe Little Proferらしい。 まだ最初の方しか読めていない。ややこしい。 focusをあてている部分にルールを適用するその仕方を繰り返し説明しているのだけれど、なんだかよくわからない。英語の読解力がないからだろう。 もう少し読み続けてみよう。 とはいえ、Juliaが優先だと思う。