Agda と LaTeX

なんか、どうしても、Agda のsourceが LaTeX で、うまく出力されなくて。verbatim 環境で、UTF8のencodeが認識されないらしい。Agda が変なUnicode fontを使うからいけないわけなんだけど。

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda

を試すわけですが、これで、本文中は大丈夫になる。verbatim が化ける。それじゃ困るんだけど。platex 固有の問題(バグ)かも。lhs は動かんし。しばらく格闘したんですが、あきらめて、

＊　indent と改行、そして、特殊記号のescapeを行うスクリプト

http://www.ie.u-ryukyu.ac.jp/%7Ekono/pub/software/agda2latex.pl

を書きました。つまり、verbatim を使わずにすませることに。あっと、tt にするのを忘れてました。tt で動くかどうか見てないな。

Agda 、マイナーだからなぁ。