ここを読む人はどんな人？

製作者（算散士）自身が、型理論等の理論的なところがわかってないので、そういう方面を知りたい人は、ここを読んでも何も得られません。ただ、型理論も知らない製作者が、Coqをいじれるようになるまでは随分と苦労したので、

Coqをちょっといじって、定理の証明支援で遊びたいな

というひとが、ここを読むと少し遊べておもしろいかもしれません。

また、いずれは形式集合論の方で行っている証明をそのままCoqで検証していこうと思います。

もどる