agda2-mode を改造し、高速化する -この記事はTheorem Proving Advent Calendar 2011の14日目の記事です。 agda2-mode とは? Agda2 は Emacs のメジャーモード agda2-mode を持ちます。agda2-mode は Agda2 を書くのに必要不可欠な多数の機能を提供しており、これが無ければ Agda2 で証明やプログラムを記述するのがとても困難になります。 agda2-mode は、以下のような機能を提供します。 ソースコードの検査 正確なシンタックスハイライト placeholder 限定的な自動証明 コンテキストと型の表示 正規形の計算 Agda2 用の入力メソッド パターンマッチ分岐の自動生成 当然これらは Emacs Lisp で記述されていますが、その本質的な部分は Haskell で記述された Agda2 処理系を呼び出すことによって実現しています。
