定理証明支援系であるCoqは、数学の定理の形式化やソフトウェアの安全性の検証を補助するツールであり、様々な場面で用いられている。
ユーザの証明記述を補助するツールとして、インタフェースであるProof Generalや、証明過程を証明木として描画するTrafなどがある。
これらのようなユーザ支援機能を統合した環境があれば、ユーザにとってCoq使用時の利便性向上に役立つと考えられる。この環境は、エディタであるVisual Studio Codeによって実現できる可能性がある。
そこで我々は、この環境開発の試みの第一段階として、Visual Studio Codeプラグインによる、Trafの証明木描画を模した描画機能を設計した。
本発表では、今回設計した描画機能のプロトタイプについて発表する。