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

語句の真相とあやまち

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

The Little Prover

これは、LISPやSchemeに対する、The Little LisperやThe Little Schemerのような関係にある Coqに対するThe Little Proferらしい。 まだ最初の方しか読めていない。ややこしい。 focusをあてている部分にルールを適用するその仕方を繰り返し説明しているのだ…