依存型を導入した言語では，高階論理を用いた型記述によりプログラムの仕様の詳細を型で表現できるため，簡潔ながら安全なプログラムを記述しやすい．しかしながら，依存型を用いた言語では，計算による値の導出や値どうしの関係を評価することに終始する一般的なプログラミング言語とは異なり，型で表される命題の証明に相当する記述が求められる．そのため，プログラムの記述並びに読解がいずれも容易とは言い難い．本研究では，依存型を持つ関数型プログラミング言語Idrisを対象とし，プログラム中の任意の部分式に対する型を簡潔に表示し，各部分式がどのような証明に相当するかを明確に読み取れるようにするユーザ支援ツールを設計する．本発表では，本ツールの設計と実装について述べる．