CoqのtacticをOCamlで書く話 - 簡潔なQCoqのtacticをOCamlで書いてみたので、同じようなことをしたい人のためにメモ。 なお私はOCamlについてはそれほど詳しくないので、そこの正確性については注意が必要。 同じ事をしているtacticがないか探す 同じようなことを考えている人は必ずいるはず。といっても、網羅的な探し方があるわけではないので、ある程度調べて見つからなかったら自分で書いたほうが効率が良いかもしれない。 まずCoq自体にないかを調べる。Coqの基本的なtacticsは Tactics Indexに書かれている。 Coqのcontribution集に似たような内容のものがないかを調べる。contributionは の「All contribs」というリンクから一覧できる。 特に、AACTacticsは有用らしく、Ubuntuのパッケージにもなっているようだ。 ssreflectには有用なtactic/tact
