これは Theorem Prover Advent Calendar 2016 17日目の記事として書かれました. idrisは依存型を持つ純粋関数型プログラミング言語です. ちなみにアイコンはこんな感じ. *1 今月の初め, バージョン 0.99 がリリースされました. 機能もほぼ安定したといことで…