読者です 読者をやめる 読者になる 読者になる

語句の真相とあやまち

なにもないことにまつわるあれこれとか関係のないこととか

The Little Prover

照明系

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

 

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

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

 

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

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