随分遅れてcoqを少しやってみました。 それ何？ 定理証明プログラムという奴です。僕の苦手なOcamlベースです＞＜ 簡単なものならCoq内部だけで、複雑なら外部コマンドとして実行できます。 基本技 全ての技は . (ピリオド)で終わります。英語と一緒ですね。…

coqだった。あまりにアホナ間違いを繰り返す自分に嫌気がさして、定理的にプログラムを定義して、後から変換もできる、というのに惹かれたんだった。今晩当たり勉強できるかな・・・