--- a/.hgignore	Thu Feb 12 15:22:21 2015 +0900
+++ b/.hgignore	Thu Feb 12 17:44:18 2015 +0900
@@ -14,6 +14,7 @@
 *.toc
 *.cpt
 
+*.agda.replaced
 *.agdai
 *.agda~
 

--- a/agda.tex	Thu Feb 12 15:22:21 2015 +0900
+++ b/agda.tex	Thu Feb 12 17:44:18 2015 +0900
@@ -505,9 +505,8 @@
 自然数の加法の交換法則を $ \equiv $-Reasoning を用いて証明した例がリスト\ref{src:nat_add_sym_reasoning}である。
 特に n と m が1以上である時の証明に注目する。
 
-% TODO: FIXME: unicode char
 \begin{table}[html]
-    \lstinputlisting[label=src:nat_add_sym_reasoning, caption= $ \equiv $ - Reasoning を用いた証明の例] {src/nat_add_sym_reasoning.agda}
+    \lstinputlisting[label=src:nat_add_sym_reasoning, caption= $ \equiv $ - Reasoning を用いた証明の例] {src/nat_add_sym_reasoning.agda.replaced}
 \end{table}
 
 まず \verb/ (S n) + (S m)/ は + の定義により \verb/ S (n + (S m)) / に等しい。

--- a/main.tex	Thu Feb 12 15:22:21 2015 +0900
+++ b/main.tex	Thu Feb 12 17:44:18 2015 +0900
@@ -3,9 +3,10 @@
 \usepackage{mythesis}
 \usepackage{multirow}
 \usepackage{here}
-\usepackage{listings, jlisting}
+\usepackage{listings}
 \usepackage{bussproofs}
 \usepackage{amssymb}
+\usepackage[utf8]{inputenc}
 
 \setlength{\itemsep}{-1zh}
 \title{圏によるプログラムの変更の形式化}
@@ -49,7 +50,7 @@
   language={},
   tabsize=4,
   lineskip=-0.5zw,
-  morecomment={[s][]{/**}{*/}},
+  escapechar={@},
 }
 \def\lstlistingname{リスト}
 \def\lstlistlistingname{リスト目次}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/replace_agda.rb	Thu Feb 12 17:44:18 2015 +0900
@@ -0,0 +1,22 @@
+#!/usr/bin/env ruby
+
+require 'pry'
+
+replace_table = {
+  '⟨' => 'langle',
+  '⟩' => 'rangle',
+  '∎' => 'blacksquare'
+}
+footer = '.replaced'
+
+sources = Dir.glob('src/*.agda')
+
+sources.each do |src|
+  code = File.read(src)
+
+  replace_table.each do |k, v|
+    code = code.gsub(k, "@$\\#{v}$@" )
+  end
+
+  File.write(src+footer , code)
+end