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