トップ «前の日記(2005-09-22) 最新 次の日記(2005-09-24)» 月表示 編集

日々の流転


2005-09-23 [長年日記]

λ. Agdaプラグイン機構; 池上 大介

を読んだ。使う側のインターフェースはシンプルでいい感じ。external予約語で書かれた項は、型チェック時に外部ツールが呼ばれる以外はabstractが指定された項と同じ扱いなのかな。それと、FOLプラグインの使用例を見ると、外部ツールには型情報も渡しているのかな。

Tags: agda 論文